Thierry Coquand has been mainly working on the implementation Agda, of type theory. Together with Catarina Coquand, he has written a presentation of part of this implementation, presented in the workshop on Logical Framework in Paris, September 99, which presents some way of structuring proofs and definitions in type theory. He has also given a course on inductive definitions in type theory at the summer school organised by the Types Working Group.
Together with Giovanni Sambin and Silvio Valentino from Padova, Thierry Coquand and Jan Smith have investigated the role of inductive definitions in formal topology. This has resulted in a draft paper "Inductive generation of formal topologies".
Peter Dybjer has been working on reduction-free normalization for coproducts with Thorsten Altenkirch, Martin Hofmann, and Phil Scott. He presented work on how to represent von Neumann ordinals in type theory at TYPES'99. He is also working on inductive-recursive definitions in type theory (partly in collaboration with Anton Setzer). Three references are
A finite axiomatization of inductive-recursive definitions (with Anton Setzer). pages 129 - 146 in Proceedings of TLCA 1999, LNCS 1581.
A general formulation of simultaneous inductive-recursive definitions in type theory, To appear in the Journal of Symbolic Logic.
Induction-recursion and initial algebras (with Anton Setzer). In preparation.
Qiao Haiyan worked with developments in ALF and Agda. It included (1) a reduction-free normalisation function for P-ccc and some related notions in P-category theory in Agda, (2) categorical properties of natural deduction proof trees in ALF, (3) proof of the equivalence of P-categorical structures of two approaches to formalising simply typed lambda-calculus in ALF. The work was presented at the TYPES'99 workshop.
Henrik Persson and Thierry Coquand have worked on developing Buchberger's algorithm, an important algorithm for computing Gröbner bases in computer algebra, in Agda. By directly proving constructively the existence of Gröbner bases in Agda, using a constructive proof of Dickson's lemma obtained from a classical proof by open induction, an integrated version of the algorithm was obtained [1]. They have also worked on formalising the polynomial ring in Agda. By using universal property, the formalisation is very independent of the concrete representation of the data-type of polynomials. The work on obtaining constructive proofs from classical proofs, with applications to problems concerning termination in rewriting, and the work on structuring proofs using abstractions formed the core of Henrik Persson's PhD thesis [2].
[1] Thierry Coquand, Henrik Persson "Gröbner Bases in Type Theory" in Selected papers from Types'99, LNCS 1657, pp 33-46, Springer-Verlag, 1999.
[2] Henrik Persson "Type Theory and the Integrated Logic of Programs", PhD thesis, Chalmers University and University of Göteborg, June 1999.
Aarne Ranta was first at XRCE (Xerox Research Centre Europe), later in Gothenburg, Ranta worked on GF (Grammatical Framework), which is a Logical Framework extended into a grammar formalism. In GF, the user edits interactively a lambda term, in the same way as proofs are edited in ALF. From this term, text can be generated text in different natural languages. It is also possible to parse natural languages. During a period of work in Helsinki, Ranta implemented PESCA (Proof Editor for Sequent Calculus), a teaching program designed as a companion to Sara Negri's and Jan von Plato's book Structural Proof Theory (to appear at Cambridge University Press). The cooperation between XRCE and TYPES continues in two forms: first, XRCE is an Industrial Participant of the new TYPES Working Group proposal. Second, XRCE is one of the three partners of the European project proposal APDOCS (Arbitrarily Precise Document Structures), coordinated by Ranta (Gothenburg), with the University of Durham as the third participant.
Makoto Takeyama worked on the coherence issues of equality and type dependency. To clarify their relationship to the recent development in weak n-category theory, an attempt is being made to reformulate the latter in type theory, replacing use of equality by that of dependent types.