Programming Logic in Göteborg, a summary for TFR

Contents

• 1. Background and history of the group
• 2. TFR's financial role
• 3. Programming logic and logical frameworks - an introduction
• 4. Recent results
  4.1 Proof editors
  4.2 Automatic theorem proving
  4.3 Language technology
  4.4 Computer checked programming
  4.5 Computational mathematics
  4.6 Semantics and proof theory
  4.7 Selected publications
• 5. Impact
  5.1 Impact on international research
  5.2 Impact on industrial applications
  5.3 Impact on education
• 6. Publication lists

Members of the group

1. Background and history of the group

The focus of our research has since the outset been the application of Martin-Löf's constructive type theory in computer science. Our group was (together with R. Constable's group at Cornell) the first to pursue this line of research. During the 1980's our group did a number of initial investigations (including implementing the first computer system for type theory), and wrote a book Programming in Martin-Löf's Type Theory - an Introduction which has become a standard reference in the field. During this period it also did much to make constructive type theory known to the international semantics and program correctness community for example by organizing a series of influential workshops.

Around 1984 T. Coquand and G. Huet at INRIA-Rocquencourt developed and implemented the Calculus of Constructions, an impredicative version of constructive type theory. In the middle of the 80's Martin-Löf suggested monomorphic type theory as a logical framework. Similar ideas were proposed in Edinburgh by G. Plotkin and his coworkers.

Together these ideas led to the creation of the EU-funded network Logical Frameworks in 1989 and its successors TYPES for proofs and programs. Our group was one of the founding sites and has had the role of a coordinator during its recent incarnation 1996-99. TYPES has become a large community of researchers presently including about 25 universities and research institutes from all over the EU as sites and subsites. It organizes among other things an annual meeting with around 100 participants.

Many of the ideas which have been extensively pursued by TYPES during the 1990's have their origin in our early investigations and also those pursued by G. Huet's group at INRIA. Coquand's move to Gothenburg and the resulting interaction between him and other members of our group led to the first implementation of the ALF-system in 1990. This was soon followed by a new, more powerful version, which has been used for extensive experiments in formalization ranging over a variety of different topics in computer science and mathematics.

Even though the focus and common denominator of our work is constructive type theory and its applications, it should be emphasized that we cover a broad range of topics from the practical (such as the design of window interfaces) to the theoretical (including topics on the border between computer science and logic). We see the intimate interaction between our work on the theory, use, and implementation of systems based on type theory as one of the cornerstones of our work.

We also repeatedly branch into related areas including other approaches to program derivation and verification, automatic theorem proving in general, applications in linguistics, computer algebra, semantics of programming languages, etc. We have since 1989 had a strong involvement in another EU-supported network of researchers, the CLICS-project which focusses on topics in semantics and other applications of Categorical Logic in Computer Science. We have been the coordinating site of the CLICS-community since 1995. In this role we have initiated the follow-up project APPSEM (Applied Semantics) which has been funded by the EU since 1998. The aim of APPSEM is to improve communication between theoretical semanticists and people working on more practical aspects of the design and implementation of programming languages.

2. TFR's financial role

Expenses

The adminstrative overhead which we pay to the various organisational layers  on top of us sum up to around 50 % of the salaries. This pays computers, secretaries, office space etc.

The cost for travel is around 100 000 crowns per year.

How important was the support of TFR?

It is a major problem for us that university research funding does not cover reasonable time for research for academic staff, even at the professorial level. Our strategy has been to use TFR funding mainly to compensate for this.

Of course, it is a familiar experience that emerging scientific fields, even those of great importance for education and to society, have difficulties in competing with established disciplines for scarce research resources. But even with this in mind, both Chalmers and the University have been slow in building up research in Computing. The University was probably the last big university in western Europe to have a professor in Computer Science. However, we still have to use this grant to pay part of his research.

The two universities now have new leadership and we are expecting a lot from their plans of building a common "IT university".

TFR is the only funding body in Sweden which supports fundamental research in Computing. They are alone in doing a careful scientific evaluation.

3. Programming logic and logical frameworks - an introduction

Programming logic addresses the central problems in constructing and reasoning about programs taking semantics into account. To explain this, we consider the two kinds of mathematical entities that are of particular interest to the practicing programmer: specifications and programs. Here we understand a specification as a description of what a program should accomplish without unnecessary constraints as to how this is accomplished. Thus we need at least two notations: the specification language, which should make it convenient to express programming tasks and properties of programs, and the programming language, which should make it convenient to express algorithms. These two languages serve quite different purposes and the distinction between them should not be blurred. On the other hand, the two should be designed to work smoothly together and thus support the programmer in the process of constructing provably correct programs. The design and analysis of this mathematical framework for programming is a central problem in programming logic.

An attractive possibility is to base a programming logic on the Curry-Howard correspondence between types and propositions and between programs and proofs. This correspondence makes it possible to interpret any proposition in predicate logic as a type in a sufficiently rich type theory. A proof of the proposition then corresponds to an object of the type. In the case that the proposition expresses the specification of a program, the proof thus contains a program satisfying this specification. This idea and its ramifications forms the basis of much of our work. It is interesting to note here the relevance of this approach to the recent strong interest in ``proof-carrying code'', prompted by the need to verify mobile code obtained over the Internet. Type theory offers the alternative paradigm of ``program-carrying proofs'' - complete objects including security proofs from which the computational content can be extracted.

A wide variety of formal systems is of interest to systems designers, including operational semantics, lambda-calculi, sequent calculi, type theories, first- and higher-order logics, Hoare logics, relevance and linear logics, and modal and temporal logics. It is therefore desirable to develop a unifying theory of formal systems that allows one to give a concise specification of the object logic. A logical framework is such a unifying theory; it provides a notation and calculus for specifying logics. It is not yet clear whether a single metalogical system can be found that encompasses all formal systems of interest. Candidates for such a system are various versions of Martin-Löf's logical framework and Coquand's and Huet's Calculus of Constructions.

In addition to the obvious advantage of conceptual simplicity of having a general logical framework, such a theory offers the possibility of implementing a logic independent proof development environment. Such a system accepts a specification of a particular logic and can then be used for developing machine-checked proofs in this logic. This eliminates, in large measure, the redundancy between implementations, and one can rapidly prototype systems for a variety of logics. This is important, since the implementation of a proof development system using modern interface technology is a major task. In our group we have developed a family of implementations of logical frameworks based on a common paradigm for proof construction: that the user interactively builds a proof by direct manipulation on screen (using mouse and menus) of a proof object representing the incomplete proof. Extensive experience with use of the systems, both in our group and at other sites, has convinced us of the efficiency and conceptual simplicity of this approach.

At this point we want to point out the connections with two other fields with long traditions in machine-developed mathematics, namely automatic theorem-proving and computer algebra. Theorem-provers can provide automatic proofs of some theorems from restricted domains, while computer algebra systems can perform extensive computations, but without proof. There are obvious opportunities for fruitful interaction with both these fields, for the benefit of all parties.

Developing completely formal proofs is a major challenge for any non-trivial problem. However, an encouraging experience in the field of programming is that extending a program, which is a completely formal algorithmic description, to an annotated version which also provides machine-checked proof of crucial properties of the program, is often not a major additional effort. In mathematics in general, the search for formal proofs often suggests or requires alternative routes of development of the theory, which may be advantageous also for informal presentation.

4. Recent results

• Proof editors. Building on previous experience we have developed a new type theory system Agda and an interface Alfa for it. The whole system is implemented in Haskell and the object language can also be seen as an extension of core Haskell with dependent types.
• Automatic theorem proving. A prototype implementation of a powerful automatic theorem prover for constructive type theory has been implemented by T. Tammet. T. Tammet also won the 1997 and 1998 theorem proving competitions held at the CADE conference.
• Language technology. A. Ranta, who has joined the group this year, has applied constructive type theory to the analysis of natural language. He came to us from Xerox where he started to develop the grammar formalism GF based on type theory.
• Type theory and programming. Much of the early work of the group was concerned with the application of type theory in programming. Recent experiments in this direction use our type theory systems ALF, Agda, and Alfa.
• Computational matematics. We have also used our systems for developing a range of examples in formal topology, metamathematics, computational category theory, and computational algebra. In the long term we believe that developments of computational mathematics will also have an impact on education: algorithms and formal proofs of theorems in elementary mathematics would be an integral part of an "electronic textbook".
• The formal system of type theory, its semantics and proof theory. We have continued our work on extending type theory with inductive definitions and pattern matching and studying its semantics. Other extensions of recent interest concern records types and subtyping. Furthermore, we have made new contributions to the topics of extracting computational content from proofs in classical logic; normalization by evaluation; and constructive ordinals.

4.1 Proof editors

In 1998, L. Augusstson designed a functional language with dependent types, Cayenne, and implemented a compiler for it. To profit from this work the language has changed to be more similar to Cayenne. A few obstacles still remains however to make them completely compatible. Also Cayenne profits from our work since Cayenne-programs can be developed in our system. The current implementation, Agda, written in Haskell by C. Coquand, consists of an incremental type checker, a termination checker, an interpreter, a constraint solver, a pretty printer and help functions.

The user can interact with Agda through an emacs-interface, designed by D. Synek, or a graphical interface, Alfa, written by Th. Hallgren.
This graphical interface improves on ALF with at least the following points:

• More flexible user interaction: most editing operations can be performed either with the mouse or the keyboard, reducing the amount of switching between keyboard and mouse and thus speeding up the editing process.
• More user control of proof presentation: this includes simple pretty printing features, like argument hiding, infix operators and quantifier notation, and also the possibility to present proofs in natural deduction style.

4.2 Formal verification and automated theorem proving

• his theorem prover Gandalf; the prover won first place 1997 and 1998 in the international competition of first-order provers organised at the CADE conferences,
• integrating Gandalf with ALF, this was partly joint work with J. Smith. He also worked on combining Gandalf with the verification systems PVS and STeP.

4.3 Type theory and language technology

• The powerful logic of type theory has provided solutions to problems of semantics such as anaphora, presupposition, and the structure of texts.
• The type system with dependent types makes it possible to describe the syntax of natural languages with a greater precision than type systems without dependent types.
• The theory and techniques of interactive syntax editing, originally developed for formal expressions such as proof terms, suggest a new mode of linguistic processing, often more appropriate than fully automatic methods.
• The task of building natural-language interfaces to proof editors is an interesting testing ground to linguistic theories.
• The use of typed functional programming languages provides a clear and high-level, yet expressive and efficient, way of implementing linguistic theories.

4.4 Computer checked programming

• N. Szasz's theory of specifications, programs, and proofs.
• A. Bove's type-theoretic analysis of a unification algorithm
• C. Gonzalia's initial investigations of relational programming in type theory following the allegory-based approach of Bird and de Moor.
• H. Persson's integrated development of Buchberger's algorithm,
• P. Dybjer and A. Setzer's formulation of type theory paving the way for writing generic programs.

Fom the beginning, our group has had strong connections with research in functional programming. One current research direction is to analyse how to extend the core of a functional programming language such as Haskell with dependent types. One important motivation is that this gives a clean approach to modules. Other suggested benefits include code optimization, having better control of space use, being more appropriate for "metaprogramming", and being more self-documented. An example of a language to be used in this way is L. Augustsson's Cayenne. As already explained, Cayenne is formally very close to the language used in our interactive proof system - the difference is that it is to be used as an ordinary functional language. (L. Augustsson is not an official member of the group but has worked with us for many years. His work on Cayenne can be viewed as a combination of our group's insights about dependent type theory and his insights about lazy functional programming languages and their implementation techniques.)

A workshop on Dependent Types in Programming was organized by us earlier this year with about 50 participants from Europe and some from the US.

4.5 Type Theory and computational mathematics

• Formal topology J. Cederquist in his thesis has proved formally a localic version of Hahn-Banach's theorem. This was a complex example, which provided a good test example for our system, and a motivation for the addition of a module system to type theory, which in now presented in the paper on Structured Type Theory. We are working together with the logic group of Padua on inductive definitions and studying first-order logic using formal topology. We have given an application of constructive completeness to constructive proofs of conservativity.
• Metamathematics C. Coquand developped in her thesis a formalised development of a substitution calculus. This calculus is closely related to the one used in our implementation of type theory.
• Computational category theory P. Dybjer and his students have developed non trivial proofs of various coherence theorems. These examples are closely connected to the analysis of normalisation proofs, and coherence problems that appear in the analysis of type theory.
• Computational algebra H. Persson in his PhD thesis has developed Buchberger algorithms in type theory. The algorithm is extracted from a constructive proof of the existence of a Grobner basis. The analysis of the feasibility of this approach is not finished yet, but this work has already provided motivations for various techniques of constructivisation of proofs in algebra, closely connected to the technique of dynamical algebra (H. Lombardi, M.F. Coste-Roy), and suggested for instance a simple constructive proof of a fundamental theorem of Kronecker.

4.6 The formal system: its semantics and proof theory

Inductive definitions and pattern matching in Type Theory. The most important development of the formal system concerns the introduction of a general system of inductive definitions in the context of dependent types. We have in particular invented a new notion of inductive-recursive definition and investigated its set-theoretic semantics. The resulting theory is at the same time a rich functional language and a strong set theory (even including analogues of large cardinals). The theory is not yet stable: we are still experimenting with different notions of inductive definitions and pattern matching in our proof assistant Agda.

Subtyping and record types. Gustavo Betarte and Alvaro Tasistro, invistigated the extension of type theory with record types and subtypings. Some experiments with record types are carried out in Agda.

Computational content of classical logic. We have investigated different ways of extracting computational content from proofs in classical logic. One approach uses an infinitary sequent calculus. Another uses formal topology for reformulating certain classical proofs in a constructive setting.

Normalization by evaluation. This is a new approach to normalization by intuitionistic model construction. We have in a series of papers (C. Coquand, T. Coquand and P. Dybjer, I. Beylin and P. Dybjer, D. Cubric, P. Dybjer, and P. Scott) investigated this approach and its connection with category theory. The approach gives rise to efficient normalization algorithms which have found use in partial evaluation.

Ordinals in Type Theory Investigations of ordinals are investigation of strong induction principles, theoretical work which historically was very important for the creation of type theory. Here T. Coquand and P. Dybjer have been collaborating with P. Hancock (Edinburgh) and A. Setzer (Uppsala) and developed two approaches: ordinals as functionals and ordinals as universes.

4.7 Selected publications

1. Th. Coquand, Computational Content of Classical Logic, in A. Pitts and P. Dybjer, eds, Semantics and Logics of Computation, pp 33-78, Publications of the Newton Institute, 1997.  [compressed ps file]

2. B. Nordström, K. Petersson, and Jan M. Smith, Martin-Löf's Type Theory, to appear as a chapter in S. Abramsky, D. M. Gabbay, and T. S. Maibaum, eds, Handbook of Logic in Computer Science, Oxford University Press,  [dvi file]

3. Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, to appear in Journal of Symbolic Logic.  [ps file]

4. Aarne Ranta, Type-Theoretical Grammar, ISBN 019853857X, Oxford University Press, 1994. [OUP catalogue entry]

5. T. Tammet, Gandalf, Journal of Automated Reasoning, vol. 18, no. 2, pp 199-204, 1997.  [ps file]

5. Impact

5.1 Impact on international research

The TYPES-community. The group has had a key role in founding a new community, the TYPES-community. The goal of this community are much the same as those of the programming logic group: the development, use, and metatheory of type theory based programming and proof systems. The TYPES community has been established since 1989 when the first of a series of EU-funded projects was approved. Our group was one of the founding members and has held the coordinatorship for the last three years. TYPES has as members about 25 universities and research institutes. It organizes an annual meeting with about 100 participants. We should here also mention that another key starting point for TYPES was the early work by Coquand (with Huet) on the definition and implementation of the Calculus of Constructions. This work was carried out while Coquand was still at INRIA Rocquencourt and forms the origin both of the theory behind and the implementation of the Coq and Lego systems developed in the TYPES project at INRIA and Edinburgh respectively.

The CLICS- and APPSEM-communities. The group has also been involved in theory development in the more general area of semantics and logics of programs. One example of this is our involvement in the CLICS (Categorical Logic in Computer Science) project, another EU-funded series of projects which started in 1989. The aim of this project was to improve the communication between mathematicians and theoretical computer scientists, and in particular to investigate applications of category theory.

Our group took over the coordinatorship of this group in 1995 and initiated the follow-up project APPSEM (Applied Semantics).

5.2 Impact on industrial applications

We recently hired Daniel Friedlender who is going to cooperate with Prover, a swedish software company. The company, founded by Gunnar Stålmarck is using his algorithm for automatic theorem proving in large industrial verifications.

Natural language technology. Aarne Ranta's system GF (Grammatical Framework) was developed at Xerox (XRCE). The cooperation with XRCE has led to a joint European project proposal, APDOCS (Arbitrarily Precise Document Structures), with the University of Durham as third partner.

5.3 Impact on Education

Undergraduate Education

The course had more than 50 students who were able to do substantially more complicated proofs than the students of previous years; in the evaluation of the course, the students were very positive to these computer exercises.

We want to develop these ideas in other areas of mathematics as well, in particular those that have applications in computer science. We are coordinating an application ``Computer tools for mathematical education'' for the EU programme Future and Emerging Technologies; this project will be aiming at using type theory systems for teaching undergraduate mathematics.

Postgraduate Education

Publication lists

It is also worth remarking that our proof assistants ALF and Agda / Alfa, available via ftp, are now being used in several academic sites.

Ph. D. theses supervised by researchers of the group

1. Jan Cederquist, supervisor: Jan M. Smith, Pointfree approach to Constructive Analysis in Type Theory, Chalmers University of Technology and University of Göteborg, 1997.

2. Alvaro Tasistro, supervisor: Bengt Nordström, Substitution, Record Types and Subtyping in Type Theory, with Applications to the Theory of Programming, Chalmers University of Technology and University of Göteborg, 1997.

3. Verónica Gaspes, supervisor: Bengt Nordström, A Type Theoretical Analysis of some Aspects of Programming, Chalmers University of Technology and University of Göteborg, 1997.

4. Nora Szasz, supervisor: Bengt Nordström, A Theory of Specifications, Programs and Proofs, Chalmers University of Technology and University of Göteborg, 1997.

5. Daniel Fridlender, supervisor: Thierry Coquand, Higman's Lemma in Type Theory, Chalmers University of Technology and University of Göteborg, 1997.

6. Gustavo Betarte, supervisor: Björn von Sydow, Dependent Record Types and Algebraic Structures in type Theory, Chalmers University of Technology and University of Göteborg, 1998.

7. Henrik Persson, supervisor: Thierry Coquand, Type Theory and the Integrated Logic of Programs, Chalmers University of Technology and University of Göteborg, 1999.

Licentiate theses supervised by researchers of the group

1. Ilya Beylin, supervisor: Peter Dybjer, An ALF Proof of Mac Lane's Coherence Theorem, Chalmers University of Technology and University of Göteborg, 1997.

2. Ana Bove, supervisor: Björn von Sydow, Programming in Martin-Löf Type Theory: Unification - A non-trivial Example, Chalmers University of Technology and University of Göteborg, 1999.

Theses and Monographs

1. Magnus Carlsson and Thomas Hallgren, Fudgets -- Purely Functional Processes with applications to Graphical User Interfaces. PhD Thesis, Department of Computing Science, Chalmers University of Technology, S-412 96 Göteborg, Sweden, March 1998.

Collections

1. Andrew M. Pitts and Peter Dybjer, eds, Semantics and Logics of Computation, Publications of the Newton Institute, Cambridge University Press, 1997.

2. Giovanni Sambin and Jan M. Smith, Twenty-Five Years of Constructive Type Theory, Oxford University Press, 1998.

Published articles in refereed journals/conference proceedings

1. G. Barthe, J. Hatcliff, and M.H. Sørensen, A notion of classical pure type system, in S. Brookes and M. Mislove, eds, Proceedings of MFPS'97, Electric Notes in Theoretical Computer Science, vol. 6, 1997.

2. G. Barthe and M.H. Sørensen, Domain-free pure type systems, in S. Adian and A. Nerode, eds, Proceedings of LFCS'97, LNCS 1234, pp 9-20, 1997.

3. G. Barthe, J. Hatcliff, and M.H. Sørensen, Reflections on reflections, in H. Glaser, P. Hartel and H. Kuchen, eds, Proceedings of PLILP'97, LNCS 1292, pp 241-258, 1997.

4. G. Barthe and F. van Raamsdonk, Termination of algebraic type systems: the syntactic approach, in M. Hanus and J. Heering, eds, Proceedings of ALP'97, LNCS 1298, pp 174-193, 1997.

5. G. Barthe, F. Kamareddine and A. Ríos. Explicit substitutions for the lambda-delta calculus. In M. Hanus and J. Heering, eds, Proceedings of ALP'97, LNCS 1298, pp 209-223, 1997.

6. G. Barthe, J. Hatcliff, and P. Thiemann, Monadic Type Systems: Pure Type Systems for Impure Settings, in Proceedings of HOOTS'97, Electronic Notes in Theoretical Computer Science, vol 10, 1997.

7. G. Barthe, The relevance of proof-irrelevance, in Proceedings of ICALP'98, LNCS 1443, 1998.

8. G. Betarte and A. Tasistro, Extension of Martin-Löf's type theory with record types and subtyping, in Twenty-Five Years of Constructive Type Theory, Oxford University Press, 1998.

9. Gustavo Betarte, Dependent Record Types, Subtyping and Proof Reutilization, accepted to Journal of Functional Programming Language.

10. A. Bove and P. Severi, Alpha Conversion in Simply Typed Lambda Calculus, in Proceedings of WOLLIC'99, Rio de Janeiro, Brazil, May 1999.

11. J. Cederquist and Th. Coquand, Entailment Relations and Distributive Lattices, to appear in Proceedings of Logic Colloquium 1998.

12. J. Cederquist,Th. Coquand, and S. Negri, The Hahn-Banach Theorem in Type Theory, in Twentyfive years of Constructive Type Theory, Oxford University Press, 1998.

13. J. Cederquist, An Implementation of the Heine-Borel Covering Theorem in Type Theory, in Types for Proofs and Programs, Selected papers from TYPES'96, LNCS 1512, pp 46-??, 1998.

14. C. Coquand and Th. Coquand, Structured Type Theory, in Proceedings of Logical Frameworks and Meta-languages, Paris, September 1999.

15. Th. Coquand and M. Hofmann, Applications of a representation theorem to subsystems of arithmetics, special issue of Mathematical Sructures in Computeter Science, vol. 9, no. 4, Special Issue on "Lambda-Calculus and Logic" in Honour of Roger Hindley, 1999.

16. Th. Coquand, Computational Content of Classical Logic, in A. Pitts and P. Dybjer, eds, Semantics and Logics of Computation, Publications of the Newton Institute, pp 33-78, 1997.

17. Th. Coquand, Formal Iterated Function Systems, to appear in Electronic Notes in Theoretical Computer Science.

18. Th. Coquand, A Formal Space of Ultrafilters, accepted to Pure and Applied Logic.

19. Th. Coquand, S. Sadocco, G. Sambin, and J. M. Smith, Formal Topologies on the Set of First-Order Formulas, to appear in Journal of Symbolic Logic.

20. Th. Coquand and H. Persson, Gröbner Bases in Type Theory, in Types for Proofs and Programs, Selected papers from TYPES'98, LNCS 1657, 1999.

21. Th. Coquand and E. Palmgren, Intuitionistic choice and classical logic, accepted for Archive for Mathematical Logic 1997.

22. Th. Coquand and P. Dybjer, Intuitionistic model constructions and normalization proofs, Mathematical Structures in Computer Science, vol. 7, no. 1, pp 75-94 1997.

23. Th. Coquand, Minimal invariant spaces in formal topology. Journal of Symbolic Logic, vol. 62, no. 3, pp 689-698, 1997.

24. Th. Coquand and H. Persson, A Proof Theorerical Analysis of Zantema's Problem, in Proceeding of CSL'97, LNCS 1414, pp 177-188, 1998.

25. Th. Coquand, Two applications of Boolean models, Archive for Mathematical Logic, vol. 37, pp 143-147, 1998.

26. Th. Coquand and H. Persson, Valuations and Dedekind's Prague Theorem, to appear in Journal of Pure and Applied Logic.

27. P. Dybjer and A. Setzer, A finite axiomatization of inductive-recursive definitions, in Proceedings of TLCA 1999, pp 129-146, LNCS 1581, 1999.

28. Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, 1997, to appear in the Journal of Symbolic Logic.

29. D. Cubric, P. Dybjer, and P. Scott, Normalization and the Yoneda embedding, Mathematical Structures in Computer Science, vol. 8, pp 153-192. 1998.

30. Peter Dybjer, Representing inductively defined sets by well-orderings in Martin-Löf's type theory, Theoretical Computer Science, vol. 176, pp 329-335, 1997.

31. Daniel Fridlender, Higman's Lemma in Type Theory, in Types for Proofs and Programs, Selected papers from TYPES'96, LNCS 1512, pp 112-133, 1998.

32. Daniel Fridlender, An Interpretation of the Fan Theorem in Type Theory, in Types for Proofs and Programs, Selected papers from TYPES'98, LNCS 1657, 1999.

33. D. Fridlender and M. Indrika, Do we need dependent types?, to appear in Journal of Functional Programming.

34. M. Indrika, Logical Relations in Circuit Verification, to appear in Proceedings of ASIAN'99, LNCS.

35. Y. Kinoshita, A. J. Power, and M. Takeyama, Sketches, in Proceedings of MFPS XIII, Electric Notes in Theoretical Computer Science, vol. 6, 1997, extended version to appear in Journal of Pure and Applied Algebra.

36. Y. Kinoshita, P. W. O'Hearn, A. J. Power, M. Takeyama, and R. D. Tennent, An axiomatic approach to binary logical relations with applications to data refinement, Theoretical Aspects of Computer Software, LNCS 1281, 1997

37. B. Nordström, K. Petersson, and Jan M. Smith, Martin-Löf's Type Theory, to appear as a chapter in Handbook on Logic in Computer Science, Oxford University Press.

38. Christophe Raffalli, A semantical Storage Operator Theorem for all Types, Annals of Applied and Pure and Applied Logic, vol. 91, no. 1, pp 17-31, 1998.

39. P.  Mäenpää and A. Ranta, The type theory and type checker of GF, Colloquium on Principles, Logics, and Implementations of High-Level Programming Languages, in Proceedings of Workshop on Logical Frameworks and Meta-languages, Paris, 1999. Available in gzipped postscript.

40. Tanel Tammet, Gandalf, Journal of Automated Reasoning, vol. 18, no. 2; pp 199-204, 1997.

41. T. Tammet and J. Smith, Optimised encodings of fragments of type theory in first order logic, Journal of Logic and computation, vol. 8, no. 6, pp 713-744, 1998.

42. Tanel Tammet, Resolution, inverse method and the sequent calculus, in Computational Logic and Proof Theory, in Proceedings of the 5th Kurt Gödel Colloquium KCG'97, Vienna, LNCS 1289, pp 65-83. 1997.

43. Tanel Tammet, Towards efficient subsumption, in Proceedings of of the Conference on Automated Deduction CADE-15, LNCS 1421, 1998.

44. Alvaro Tasistro, Abstract Insertion Sort in Extension of Type Theory with Record Types and Subtyping, in Types for Proofs and Programs, Selected Papers from TYPES'96, LNCS 1512, 1998.