1. The logical theory of constructions P. Aczel and D. Carlisle; 2. The
Boyer-Moore theorem prover and Nuprl: an experimental comparison D. Basin
and M. Kaufmann; 3. Girard normalisation proof in LEGO S. Beradi; 4. A plea
for weaker frameworks N. de Bruijn; 5. Deliverables: an approach to program
development in the Calculus of Constructions R. Burstall and J. McKinna; 6.
Finding computational content in classical proofs R. Constable and C.
Murthy; 7. An algorithm for testing conversion in type theory T. Coquand;
8. A proof synthesis algorithm for testing conversion in type theory G.
Dowek; 9. Inductive sets and families in Martin-Löf's type theory and their
set-theoretic semantics P. Dybjer; 10. Encoding a dependent-type
lambda-calculus in a logic A. Felty and D. Miller; 11. Nederpelt's calculus
extended with a notion of context as a logical framework P. de Groote; 12.
Models of partial induction L. Hallnäs; 13. Goal-directed proof
construction in type theory L. Helmink; 14. Elf: a language for logic
definition and verified meta-programming E. Pfenning; 15. Investigations
into proof-search in a system of first-order dependent function types D.
Pym and L. Wallen; 16. The role of elimination inferences in a structural
framework P. Schroeder-Heister.
