TYPES 1995: Torino, Italy

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