TYPES 1995: Torino, Italy

• Gilles Barthe:
  Implicit Coercions in Type Systems. 1-15
  Electronic Edition (link) BibTeX
• Gilles Barthe, Mark Ruys, Henk Barendregt:
  A Two-Level Approach Towards Lean Proof-Checking. 16-35
  Electronic Edition (link) BibTeX
• Ulrich Berger, Helmut Schwichtenberg:
  The Greatest Common Divisor: A Case Study for Program Extraction from Classical Proofs. 36-46
  Electronic Edition (link) BibTeX
• Ilya Beylin, Peter Dybjer:
  Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. 47-61
  Electronic Edition (link) BibTeX
• Jan Cederquist, Sara Negri:
  A Constructive Proof of the Heine-Borel Covering Theorem for Formal Reals. 62-75
  Electronic Edition (link) BibTeX
• Thierry Coquand, Jan M. Smith:
  An Application of Constructive Completeness. 76-84
  Electronic Edition (link) BibTeX
• Cristina Cornes, Delphine Terrasse:
  Automating Inversion of Inductive Predicates in Coq. 85-104
  Electronic Edition (link) BibTeX
• Philippe Curmin:
  First Order Marked Types. 105-119
  Electronic Edition (link) BibTeX
• Peter Dybjer:
  Internal Type Theory. 120-134
  Electronic Edition (link) BibTeX
• Eduardo Giménez:
  An Application of Co-inductive Types in Coq: Verification of the Alternating Bit Protocol. 135-152 BibTeX
• Martin Hofmann:
  Conservativity of Equality Reflection over Intensional Type Theory. 153-164
  Electronic Edition (link) BibTeX
• Furio Honsell, Marino Miculan:
  A Natural Deduction Approach to Dynamic Logic. 165-182
  Electronic Edition (link) BibTeX
• Lena Magnusson:
  An Algorithm for Checking Incomplete Proof Objects in Type Theory with Localization and Unification. 183-200
  Electronic Edition (link) BibTeX
• Vincent Padovani:
  Decidability of All Minimal Models. 201-215
  Electronic Edition (link) BibTeX
• Christine Paulin-Mohring:
  Circuits as Streams in Coq: Verification of a Sequential Multiplier. 216-230
  Electronic Edition (link) BibTeX
• Aarne Ranta:
  Context-Relative Syntactic Categories and the Formalization of Mathematical Text. 231-248
  Electronic Edition (link) BibTeX
• Milena Stefanova, Herman Geuvers:
  A Simple Model Construction for the Calculus of Constructions. 249-264
  Electronic Edition (link) BibTeX
• Tanel Tammet, Jan M. Smith:
  Optimized Encodings of Fragments of Type Theory in First Order Logic. 265-287
  Electronic Edition (link) BibTeX
• Jan von Plato:
  Organization and Development of a Constructive Axiomatization. 288-296
  Electronic Edition (link) BibTeX