Researchers active in the TYPES area at Oxford are: Corin Pitcher, Charles Stewart, Dominic Hughes, Thong Wei Koh, Kwong-Cheong Wong, Guy McCusker, Hanno Nickau, Luke Ong and Lincoln Wallen.
A brief report on some recent highlights follows.
Corin Pitcher in collaboration with Søren B. Lassen have investigated variants of applicative similarity and bisimilarity for compatibility in the setting of a higher-order functional programming language with countable non-determinism [1]. Pitcher is continuing his studies into a functional programming language extended with operators that have (often unbounded) non-deterministic behaviour. Several families of applicative similarities and bisimilarities are being studied and shown to be compatible by an extension of techniques due to Howe and Ong. The extended language is used as the target of a semantics by translation of a variant of Dijkstra's guarded command language.
Charles Stewart is preparing a thesis entitled ``Classical proof theory and the lambda-mu calculus.'' Stewart and Ong have developed a coding of Felleisen's control operators and a simple exception mechanism into a CBV variant of Parigot's lambda-mu calculus, and examines the operational semantics of this calculus [2].
Stewart's thesis will examine the claim of Parigot's lambda-mu calculus to provide the computational side of a Curry-Howard like correspondence for classical logic. The principal contributions are to present some refinements of the lambda-mu calculus that facilitate a strong correspondence with a natural presentation of classical proof theory, and to consider the extension of the correspondence to the predicate calculus by extending Martin-Loef's type theory.
Dominic Hughes, who also attended the TYPES meeting in Aussois, works in game semantics. His paper [3] examines system F from this perspective. The Types meeting was of great value to him especially discussions on the validity of the eta rule for system F. A new idea for a games model for system F has been submitted [4].
Thong Wei Koh has completed a thesis on term languages for various symmetrical monoidal categories, succeeding in giving an elegant internal language for categories which model multiplicative linear logic with units. The language features a local reduction operation and accurate and simple modelling of the units [5].
Guy McCusker an Samson Abramsky have developed a general construction of models of call-by-value computation from models of call-by-name. It is essentially a matter of programming in a suitable type theory, but presented in terms of categorical models. The construction is applied to categories of games, yielding new fully abstract models of the call-by-value functional language PCFv, and a language with dynamically allocated store similar to the references of Standard ML [6].
Wallen, Pym (Queen Mary And Westfield site) and Ritter (Birmingham site) have exchanged several visits. They have been working on various aspects of proof-search in classical and intuitionistic logics, leading to the publication of papers in both the Tableaux and CADE proceedings [7,8]. Central to this work is the use of variants of lambda-mu to code classical derivations which are then examined for intuitionistic substructure. This work has recently been extended to first-order intuitionistic logic and a multiple conclusioned version of lambda-Pi by Wallen and KC Wong. A treatment of disjunction has been developed and its semantics investigated by Pym and Ritter.
[1] Søren B. Lassen & Corin Pitcher. Similarity and Bisimilarity for Countable Non-Determinism and Higher-Order Functions (to appear in ENTCS).
[2] Charles Stewart and Luke Ong. A Curry-Howard foundation for functional computation with control. In Proc. POPL '97.
[3] Dominic Hughes. Games and Definability for System F. In the proceedings of the conference Logic in Computer Science, Warsaw, 1997.
[4] Dominic Hughes. A PER model of system F constructed over linear games. (Submitted.)
[5] Thong Wei Koh. Multiplicative linear type theories. DPhil thesis, Oxford. (Submitted.)
[6] Samson Abramsky and Guy McCusker. Call-by-value games. In Proceedings of CSL '97, 1997, Springer-Verlag, LNCS (to appear).
[7] Ritter, Pym and Wallen. On the intuitionistic force of classical search. In Proc. Intl. Workshop on Tableaux, Miglioli, Moscato, Mundici, Ornaghi (eds), LNCS 1071, pp295-311, 1996.
[8] Ritter, Pym and Wallen. Proof terms for classical and intuitionistic resolution. In Proc CADE-13, Slaney and McRobbie (eds), LNCS 1104, pp17-31, 1996.