The report from Chalmers consists of a list of reports from members of the WG.
Gustavo Betarte is working on a formulation of Martin-Löf's type theory extended with record types and subtyping. He has studied meta-theoretic properties of the calculus and has implemented a type checking algorithm for the formal verification of its judgements. He has formalized examples from abstract algebra, using the implementation. The work is part of his forthcoming Ph.D. thesis.
Extension of Martin-Löf's type theory with record types and subtyping (with Alvaro Tasistro). To appear in "25 Years of Constructive Type Theory", Oxford University Press, 1997. URL: "http://www.cs.chalmers.se/ gustun/papers/venezia.ps.gz" Dependent Record Types, Subtyping and Proof reutilization. In the online proceedings of the Working Group TYPES workshop "Subtyping, inheritance and modular development of proofs", held at Durham, England, 1997.URL: "http://www.cs.chalmers.se/ gustun/papers/durham.ps.gz"
Ana Bove has done a formalisation in Half which shows that "well typed expression cannot go wrong". The language used is a small (typed) functional language containing variables, abstractions, applications, fix points, boolean values and conditionals. Actually, the proof is made for programs, i.e. closed expressions.
Jan Cederquist has worked on formal free topology and has developed the Hahn-Banach theorem i the Half system. He finished his Ph.D thesis in May.
An implementation of the Heine-Borel covering theorem in type theory, To appear in LNCS, E. Gimenez and C. Paulin eds., selected papers of the Types meeting, Aussois, 1996. The Hahn-Banach Theorem in Type Theory (written together with Thierry Coquand and Sara Negri), To appear in the proceedings of Twenty-Five years of Constructive Type Theory, G. Sambin and J. Smith eds., Oxford University Press. A Machine Assisted Proof of the Hahn-Banach Theorem, Chalmers University of Technology and University of Göteborg, 1997. Submitted to JAR.A Pointfree Approach to Constructive Analysis in Type Theory. Ph. D. thesis
Thierry Coquand and Henrik Persson have performed case-studies in extraction of constructive proofs from classical proofs, something which is important in order to reason about computations inside type theory. The case-studies comes from rewriting and algebra. In rewriting, they extracted constructive proofs of Zantema's problem, termination of recursive path ordering, and preservation of strong normalisation for an explicit substitution calculus, the last two results are still work in progress. In algebra, they extracted constructive proofs of Hilbert's basis theorem, which they hope to use for a completely integrated development of Groebner basis in type theory."
Th. Coquand and H. Persson, "A Proof-Theoretical Investigation of Zantema's Problem", CSL'97 Preliminary Proceedings
Formal topology has proved to be a promising way to express, in type theory, a number of different areas of mathematics. Thierry Coquand and Jan Smith have investigated different coverings for first order logic.
Thierry Coquand, Sara Sadocco, Giovanni Sambin, and Jan M. Smith. "Formal Topologies on the Set of First-Order Formulae", draft.
Peter Dybjer has worked on (i) normalization proofs based on constructive category theory and (ii) universes in type theory.
A general formulation of simultaneous inductive-recursive definitions in type theory. June 1997. To appear in the Journal of Symbolic Logic. Normalization and the Yoneda embedding. (with Djordje Cubric and hilip Scott).June 1997. To appear in Mathematical Structures in Computer Science.
Daniel Fridlender has worked on a constructive proof of Higman's lemma and on some model constructions for type theory motivated by this proof. The proof is an adaptation in type theory of the recent intuitionistic proof of Higman's lemma by Wim Veldman, for relations that may not be decidable. Daniel Fridlender has generalised the proof irrelevant model of Jan Smith to the complete logical framework. This model can be adpated to give a realisability model. He finisehd his Ph.D. thesis in October.
Higman's lemma in type theory To appear in LNCS, E. Gimenez and C. Paulin eds., selected papers of the Types meeting, Aussois, 1996. Higman's Lemma in Type Theory Ph.D. Thesis
Veronica Gaspes presented "Infinite Objects in Type Theory" at the workshop in Aussois. It was a part of her Ph.D. thesis, which she finished in June.
A Type Theoretical Analysis of Some Aspects of Programming Languages. Ph.D thesis.
For some years, the Programming Logic Group has worked on implementations of logical frameworks. The most recent version, known as Alfa, is expected to improve upon the previous version (ALF) by providing a simpler but more powerful user interface, implemented by Thomas Hallgren, and by giving the user more control of how proofs and terms are formatted. For example, proofs can be presented in natural deduction style. Whereas ALF was a hybrid implementation, with some parts implemented in Standard ML and others in C++, Alfa is written entirely in the lazy functional language Haskell, thanks to the use of the user interface toolkit Fudgets. As a result, it will be significantly smaller and thereby easier to maintain and extend.
More information:ALF: http://www.cs.chalmers.se/Cs/Research/Logic/alf/guide.html
Alfa: http://www.cs.chalmers.se/ hallgren/Alfa/
Fudgets: http://www.cs.chalmers.se/Fudgets/
Makoto Takeyama is working on program semantics in a categorical and type theoretic setting. Possible goals include:
Tanel Tammet has worked on fully automated theorem proving for type theory. The paper
T.Tammet and J.M.Smith. "Optimized Encodings of Fragments of Type Theory in First Order Logic", accepted for publication in the Journal of Logic and Computation. presents sound and complete translations of several fragments of Martin-Löf's monomorphic type theory to first order predicate calculus. The translations are optimised for the purpose of automated theorem proving in the mentioned fragments. The implementation of the theorem prover Gandalf and several experimental results are described.The paper
T.Tammet. 'A Resolution Theorem Prover for Intuitionistic Logic' , in "CADE-13", Springer LNCS 1104, pp 2-16, 1996. uses the general scheme of building resolution calculi (also called the inverse method) originating from S.Maslov and G.Mints to design and implement a resolution theorem prover for intuitionistic logic. The classical version of the same prover, called Gandalf, won the international first order prover competition CASC in 1997, seehttp://www.cs.jcu.edu.au/ tptp/CASC-14/