Types for Proofs and Programs

1. Front Matter

   PDF

2. Implicit coercions in type systems

   • Gilles Barthe

   Pages 1-15

3. A two-level approach towards lean proof-checking

   • Gilles Barthe, Mark Ruys, Henk Barendregt

   Pages 16-35

4. The greatest common divisor: A case study for program extraction from classical proofs

   • U. Berger, H. Schwichtenberg

   Pages 36-46

5. Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids

   • Ilya Beylin, Peter Dybjer

   Pages 47-61

6. A constructive proof of the Heine-Borel covering theorem for formal reals

   • Jan Cederquist, Sara Negri

   Pages 62-75

7. An application of constructive completeness

   • Thierry Coquand, Jan M. Smith

   Pages 76-84

8. Automating inversion of inductive predicates in Coq

   • Cristina Cornes, Delphine Terrasse

   Pages 85-104

9. First order marked types

   • Philippe Curmin

   Pages 105-119

10. Internal type theory

    • Peter Dybjer

    Pages 120-134

11. An application of co-inductive types in Coq: Verification of the alternating bit protocol

    • Eduardo Giménez

    Pages 135-152

12. Conservativity of equality reflection over intensional type theory

    • Martin Hofmann

    Pages 153-164

13. A natural deduction approach to dynamic logic

    • Furio Honsell, Marino Miculan

    Pages 165-182

14. An algorithm for checking incomplete proof objects in type theory with localization and unification

    • Lena Magnusson

    Pages 183-200

15. Decidability of all minimal models

    • Vincent Padovani

    Pages 201-215

16. Circuits as streams in Coq: Verification of a sequential multiplier

    • Christine Paulin-Mohring

    Pages 216-230

17. Context-relative syntactic categories and the formalization of mathematical text

    • Aarne Ranta

    Pages 231-248

18. A simple model construction for the Calculus of Constructions

    • M. Stefanova, H. Geuvers

    Pages 249-264

19. Optimized encodings of fragments of type theory in first order logic

    • Tanel Tammet, Jan M. Smith

    Pages 265-287

20. Organization and development of a constructive axiomatization

    • Jan von Plato

    Pages 288-296

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.

• Automatisches Schließen
• Beweisprüfung
• Beweistheorie
• Coq
• Monoid
• Typensysteme
• Typentheorie
• algorithm
• algorithms
• logic
• proof checking
• proof theory
• type systems
• type theory
• verification

Policies and ethics