Contents
--------

Foreword								1

Program of the workshop							3

P. Aczel, D. Carlisle.  The Logical Theory of Constructions: A formal
	framework and its implementation				19

L. Augustsson, T. Coquand, & B. Nordstrom.  A short description of
	Another Logical Framework					39

D. Basin & M. Kaufmann.  The Boyer-Moore Prover and Nuprl: An
	Experimental Comparison						43

S. Berardi.  Girard Normalization Proof in LEGO				67

A. Bundy, A. Smaill & J. Hesketh.  Turning Eureka Steps into
	Calculations in Automatic Program Synthesis			79

R. Burstall & F. Honsell.  A Natural Deduction treatment of
	Operational Semantics						89

R. Burstall & J. McKinna.  Deliverables: an approach to program
	development in the Calculus of Constructions			113

N. de Bruijn.  A plea for weaker frameworks				123

B. Constable & C. Murthy.  Finding Computational Content in Classical
	Proofs								141

T. Coquand.  An algorithm for testing conversion in Type Theory		157

P. de Groote.  Nederpelt's Calculus extended with a notion of Context
	as a Logical Framework						167

J. Despeyroux.  Theo, an interactive proof development system		181

G. Dowek.  A Proof Synthesis Algorithm for a Mathematical Vernacular	183

P. Dybjer.  Inductive Sets and Families in Martin-L\"of's Type Theory
	and Their Set-Theoretic Semantics				213

A. Felty & D. Miller.  Encoding a Dependent-Type $\lambda$-Calculus
	in a Logic Programming Language					231

J.Y. Girard.  Logic vs Logics						245

L. Halln\"as.  Models of partial inductive definitions			247

L. Helmink.  Goal Directed Proof Construction in Type Theory		259

M. Kaufmann.  DEMO of the Boyer-Moore Theorem Prover and some of its
	extensions							299

D. Miller.  An Extension to ML to Handle Bound Variables in Data
	Structures							323

N. Mendler.  A series of type theories and their interpretations in
	the logical theory of constructions				337

N. Mendler.  Quotient types via coequalizers in Martin-L\"of type
	theory								349

T. Nipkow.  A Critical Pair Lemma for Higher-Order Rewrite Systems
	and its Application to $\lambda^*$				361

C. Paulin & B. Werner.  Extracting and Executing Programs Developed
	in the Inductive Constructions System: a Progress Report	377

F. Pfenning.  Elf: A Language for Logic Definition and Verified
	Metaprogramming							391

C. Phillips.  Implementing General Recursion in Type Theory		407

R. Pollack.  Implicit Syntax						421

D. Pym & L. Wallen.  Investigations into proof-search in a system of
	first-order dependent function types				435

P. Schroeder-Heister.  The Role of Elimination Inferences in a
	Structural Framework						453

M. Coen.  Interactive Program Synthesis within ZF set theory		463

T. Coquand & J. Gallier.  A Proof of Strong Normalization For the
	Theory of Constructions Using a Kripke-Like Interpretation	479