Types for Proofs and Programs: International Workshop, TYPES '95, Torino, Italy, June 5 - 8, 1995 Selected Papers (Lecture Notes in Computer Science, 1158)

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. Implicit Coercions In Type Systems / Gilles Barthe -- A Two-level Approach Towards Lean Proof-checking / Gilles Barthe, Mark Ruys And Henk Barendregt -- The Greatest Common Divisor : A Case Study For Program Extraction From Classical Proofs / Ulrich Berger And Helmut Schwichtenberg -- Extracting A Proof Of Coherence For Monoidal Categories From A Proof Of Normalization For Monoids / Ilya Beylin And Peter Dybjer -- A Constructive Proof Of The Heine-borel Covering Theorem For Formal Reals / Jan Cederquist And Sara Negri -- An Application Of Constructive Completeness / Thierry Coquand And Jan Smith --automating Inversion Of Inductive Predicates In Coq / Cristina Cornes And Delphine Terrasse -- First Order Marked Types / Philippe Curmin -- Internal Type Theory / Peter Dybjer -- An Application Of Co-inductive Types In Coq : Verification Of The Alternating Bit Protocol / Eduardo Giménez -- Conservativity Of Equality Reflection Over Intensional Type Theory / Martin Hofmann -- A Natural Deduction Approach To Dynamic Logic / Furio Honsell And Marino Miculan -- An Algorithm For Checking Incomplete Proof Objects In Type Theory With Localization And Unification / Lena Magnusson -- Decidability Of All Minimal Models / Vincent Padovani -- Circuits As Streams In Coq : Verification Of A Sequential Multiplier / Christine Paulin-mohring -- Context-relative Syntactic Categories And The Formalization Of Mathematical Text / Aarne Ranta -- A Simple Model Construction For The Calculus Of Constructions / Milena Stefanova And Herman Geuvers -- Optimized Encodings Of Fragments Of Type Theory In First Order Logic / Tanel Tammet And Jan Smith -- Organization And Development Of A Constructive Axiomatization / Jan Von Plato. Stefano Berardi, Mario Coppo, (eds.). Includes Bibliographical References. 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 The increasing importance of mathematical software has been accompanied by a drift of mainstream mathematics towards mathematical logic and the foundations of mathematics.