TYPES 1995:
Torino,
Italy
Stefano Berardi, Mario Coppo (Eds.):
Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers.
Lecture Notes in Computer Science 1158 Springer 1996, ISBN 3-540-61780-9 
- 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
Last update Fri May 25 08:43:37 2012
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
