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