This book constitutes the thoroughly revised post-workshop proceedings of the first annual workshop held under the auspices of the ESPRIT Working Group 21900 TYPES in Aussois, France in December 1996.
The 18 revised full papers presented in the book were carefully reviewed and selected from the 30 papers accepted for presentation at the workshop. All current aspects of type theory and type systems and their applications to program verification and theorem proving are addressed; the proof systems and theorem provers dealt with include Coq, LEGO, and Isabelle/HOL.
Author(s): Eduardo Giménez, Christine Paulin-Mohring (eds.)
Series: Lecture Notes in Computer Science 1512
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1998
Language: English
Pages: 380
Tags: Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Programming Languages, Compilers, Interpreters; Artificial Intelligence (incl. Robotics)
Introduction....Pages 1-8
Coercion synthesis in computer implementations of type-theoretic frameworks....Pages 9-27
Verification of the interface of a small proof system in coq....Pages 28-45
An implementation of the Heine-Borel covering theorem in type theory....Pages 46-65
Detecting and removing dead-code using rank 2 intersection....Pages 66-87
A type-free formalization of mathematics where proofs are objects....Pages 88-111
Higman's lemma in type theory....Pages 112-133
A proof of weak termination of typed λσ-calculi....Pages 134-153
Proof style....Pages 154-172
Some algorithmic and proof-theoretical aspects of coercive subtyping....Pages 173-195
Semantical BNF....Pages 196-215
The internal type theory of a Heyting pretopos....Pages 216-235
Inverting inductively defined relations in LEGO....Pages 236-253
A generic normalisation proof for pure type systems....Pages 254-276
Proving a real time algorithm for ATM in Coq....Pages 277-293
Dependent types with explicit substitutions: A meta-theoretical development....Pages 294-316
Type inference verified: Algorithm W in Isabelle/HOL....Pages 317-332
Continuous lattices in formal topology....Pages 333-353
Abstract insertion sort in an extension of type theory with record types and subtyping....Pages 354-372
