Logical Frameworks

This volume contains the proceedings of the first international workshop on Logical Frameworks. The contributions are concerned with the application of logical reasoning and proof theory in computer science and their relevance to automatic-theorem proving and consequently topics such as artificial intelligence. It is the only source for much of this material and will be a necessary purchase for mathematicians and computer scientists undertaking research at the interface of logic and software engineering. CONTENTS......Page 6 Preface......Page 8 Introduction......Page 10 FRAMEWORKS......Page 14 Two frameworks of theories and their implementation in Isabelle......Page 16 A plea for weaker frameworks......Page 53 Nederpelt's calculus extended with a notion of context as a logical framework......Page 82 IMPLEMENTATIONS......Page 100 The Boyer-Moore Prover and Nuprl: An Experimental Comparison......Page 102 Goal directed proof construction in type theory......Page 133 Logic programming in the LF logical framework......Page 162 REPRESENTING FORMAL SYSTEMS......Page 196 Operational semantics in a natural deduction setting*......Page 198 Encoding Dependent Types in an Intuitionistic Logic......Page 228 TYPE THEORY......Page 266 An algorithm for testing conversion in Type Theory......Page 268 Inductive sets and families in Martin-L6f's type theory and their set-theoretic semantics......Page 293 PROOFS AND COMPUTATION......Page 320 Proof-search in the All-calculus......Page 322 Finding Computational Content in Classical Proofs......Page 354 LOGICAL ISSUES......Page 376 Models of partial inductive definitions......Page 378 Structural Frameworks, Substructural Logics, and the Role of Elimination Inferences......Page 398 This 1991 volume contains the proceedings of the first international workshop on Logical Frameworks.