This volume contains a refereed selection of revised full papers chosen from the contributions presented during the Third Annual Workshop held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs. The workshop took place in Torino, Italy, in June 1995.
Type theory is a formalism in which theorems and proofs, specifications and programs can be represented in a uniform way. The 19 papers included in the book deal with foundations of type theory, logical frameworks, and implementations and applications; all in all they constitute a state-of-the-art survey for the area of type theory.
Author(s): Gilles Barthe (auth.), Stefano Berardi, Mario Coppo (eds.)
Series: Lecture Notes in Computer Science 1158
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1996
Language: English
Pages: 298
Tags: Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Artificial Intelligence (incl. Robotics)
Implicit coercions in type systems....Pages 1-15
A two-level approach towards lean proof-checking....Pages 16-35
The greatest common divisor: A case study for program extraction from classical proofs....Pages 36-46
Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids....Pages 47-61
A constructive proof of the Heine-Borel covering theorem for formal reals....Pages 62-75
An application of constructive completeness....Pages 76-84
Automating inversion of inductive predicates in Coq....Pages 85-104
First order marked types....Pages 105-119
Internal type theory....Pages 120-134
An application of co-inductive types in Coq: Verification of the alternating bit protocol....Pages 135-152
Conservativity of equality reflection over intensional type theory....Pages 153-164
A natural deduction approach to dynamic logic....Pages 165-182
An algorithm for checking incomplete proof objects in type theory with localization and unification....Pages 183-200
Decidability of all minimal models....Pages 201-215
Circuits as streams in Coq: Verification of a sequential multiplier....Pages 216-230
Context-relative syntactic categories and the formalization of mathematical text....Pages 231-248
A simple model construction for the Calculus of Constructions....Pages 249-264
Optimized encodings of fragments of type theory in first order logic....Pages 265-287
Organization and development of a constructive axiomatization....Pages 288-296
