Search results for "TYPES"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Peter Aczel	On Relating Type Theories and Set Theories.	TYPES	1998	DBLP DOI BibTeX RDF
1	Joëlle Despeyroux, Pierre Leleu	A Modal Lambda Calculus with Iteration and Case Constructs.	TYPES	1998	DBLP DOI BibTeX RDF
1	Daniel Fridlender	An Interpretation of the Fan Theorem in Type Theory.	TYPES	1998	DBLP DOI BibTeX RDF	fan theorem, inductive bar, type theory
1	Thierry Coquand, Henrik Persson	Gröbner Bases in Type Theory.	TYPES	1998	DBLP DOI BibTeX RDF
1	Conor McBride	Inverting Inductively Defined Relations in LEGO.	TYPES	1996	DBLP DOI BibTeX RDF
1	Sara Negri	Continous Lattices in Formal Topology.	TYPES	1996	DBLP DOI BibTeX RDF
1	Stefano Berardi, Mario Coppo (eds.)	Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers	TYPES	1996	DBLP DOI BibTeX RDF
1	Daniel Fridlender	Highman's Lemma in theory.	TYPES	1996	DBLP DOI BibTeX RDF
1	Anthony Bailey	Coercion Synthesis in Computer Implementations of Type-Theoretic Frameworks.	TYPES	1996	DBLP DOI BibTeX RDF
1	Jean Goubault-Larrecq	A Proof of Weak Termination of Typed lambda-sigma-Calculi.	TYPES	1996	DBLP DOI BibTeX RDF
1	César A. Muñoz	Dependent Types with Explicit Substitutiuons: A Meta-theoretical development.	TYPES	1996	DBLP DOI BibTeX RDF
1	Jan Cederquist	An Implementation of the Heine-Borel Covering Theorem in Type Theory.	TYPES	1996	DBLP DOI BibTeX RDF
1	Petri Mäenpää	Semantical BNF.	TYPES	1996	DBLP DOI BibTeX RDF
1	John Harrison 0001	Proof Style.	TYPES	1996	DBLP DOI BibTeX RDF
1	Wolfgang Naraschewski, Tobias Nipkow	Type Inference Verified: Algorithm W in Isabelle/HOL.	TYPES	1996	DBLP DOI BibTeX RDF
1	Maria Emilia Maietti	The Internal Type Theory of a Heyting Pretopos.	TYPES	1996	DBLP DOI BibTeX RDF
1	Ferruccio Damiani, Frédéric Prost	Detecting and Removing Dead-Code using Rank 2 Intersection.	TYPES	1996	DBLP DOI BibTeX RDF
1	Bruno Barras	Verification of the Interface of a Small Proof System in Coq.	TYPES	1996	DBLP DOI BibTeX RDF
1	Eduardo Giménez 0001, Christine Paulin-Mohring	Introduction.	TYPES	1996	DBLP DOI BibTeX RDF
1	Paul-André Melliès, Benjamin Werner	A Generic Normalisation Proof for Pure Type Systems.	TYPES	1996	DBLP DOI BibTeX RDF
1	Gilles Dowek	A Type-Free Formalization of Mathematics where Proofs are Objects.	TYPES	1996	DBLP DOI BibTeX RDF
1	Jean-François Monin	Proving a Real Time Algorithm for ATM in Coq.	TYPES	1996	DBLP DOI BibTeX RDF
1	Alvaro Tasistro	Abstract Insertion Sort in an Extension of Type Theory with Record Types and Subtyping.	TYPES	1996	DBLP DOI BibTeX RDF
1	Alex P. Jones, Zhaohui Luo, Sergei Soloviev 0001	Some Algorithmic and Proof-Theoretical Aspects of Coercive Subtyping.	TYPES	1996	DBLP DOI BibTeX RDF
1	Tanel Tammet, Jan M. Smith	Optimized Encodings of Fragments of Type Theory in First Order Logic.	TYPES	1995	DBLP DOI BibTeX RDF
1	Vincent Padovani	Decidability of All Minimal Models.	TYPES	1995	DBLP DOI BibTeX RDF
1	Cristina Cornes, Delphine Terrasse	Automating Inversion of Inductive Predicates in Coq.	TYPES	1995	DBLP DOI BibTeX RDF
1	Jan Cederquist, Sara Negri	A Constructive Proof of the Heine-Borel Covering Theorem for Formal Reals.	TYPES	1995	DBLP DOI BibTeX RDF
1	Ilya Beylin, Peter Dybjer	Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids.	TYPES	1995	DBLP DOI BibTeX RDF
1	Furio Honsell, Marino Miculan	A Natural Deduction Approach to Dynamic Logic.	TYPES	1995	DBLP DOI BibTeX RDF
1	Gilles Barthe	Implicit Coercions in Type Systems.	TYPES	1995	DBLP DOI BibTeX RDF
1	Peter Dybjer	Internal Type Theory.	TYPES	1995	DBLP DOI BibTeX RDF
1	Aarne Ranta	Context-Relative Syntactic Categories and the Formalization of Mathematical Text.	TYPES	1995	DBLP DOI BibTeX RDF
1	Philippe Curmin	First Order Marked Types.	TYPES	1995	DBLP DOI BibTeX RDF
1	Milena Stefanova, Herman Geuvers	A Simple Model Construction for the Calculus of Constructions.	TYPES	1995	DBLP DOI BibTeX RDF
1	Christine Paulin-Mohring	Circuits as Streams in Coq: Verification of a Sequential Multiplier.	TYPES	1995	DBLP DOI BibTeX RDF
1	Gilles Barthe, Mark Ruys, Henk Barendregt	A Two-Level Approach Towards Lean Proof-Checking.	TYPES	1995	DBLP DOI BibTeX RDF
1	Martin Hofmann 0001	Conservativity of Equality Reflection over Intensional Type Theory.	TYPES	1995	DBLP DOI BibTeX RDF
1	Jan von Plato	Organization and Development of a Constructive Axiomatization.	TYPES	1995	DBLP DOI BibTeX RDF
1	Lena Magnusson	An Algorithm for Checking Incomplete Proof Objects in Type Theory with Localization and Unification.	TYPES	1995	DBLP DOI BibTeX RDF
1	Eduardo Giménez 0001	An Application of Co-inductive Types in Coq: Verification of the Alternating Bit Protocol.	TYPES	1995	DBLP DOI BibTeX RDF
1	Peter Dybjer, Bengt Nordström, Jan M. Smith (eds.)	Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers	TYPES	1995	DBLP DOI BibTeX RDF
1	Ulrich Berger 0001, Helmut Schwichtenberg	The Greatest Common Divisor: A Case Study for Program Extraction from Classical Proofs.	TYPES	1995	DBLP DOI BibTeX RDF
1	Thierry Coquand, Jan M. Smith	An Application of Constructive Completeness.	TYPES	1995	DBLP DOI BibTeX RDF
1	René M. C. Ahn	Communication Contexts: a Pragmatic Approach to Information Exchange.	TYPES	1994	DBLP DOI BibTeX RDF
1	Herman Geuvers	A short and flexible proof of Strong Normalization for the Calculus of Constructions.	TYPES	1994	DBLP DOI BibTeX RDF
1	Robert Pollack	On Extensibility of Proof Checkers.	TYPES	1994	DBLP DOI BibTeX RDF
1	Henk Barendregt, Tobias Nipkow (eds.)	Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers	TYPES	1994	DBLP DOI BibTeX RDF
1	Lawrence C. Paulson	A Concrete Final Coalgebra Theorem for ZF Set Theory.	TYPES	1994	DBLP DOI BibTeX RDF
1	Healfdene Goguen	The Metatheory of UTT.	TYPES	1994	DBLP DOI BibTeX RDF
1	Tobias Nipkow, Konrad Slind	I/Q Automata in Isabelle/HOL.	TYPES	1994	DBLP DOI BibTeX RDF
1	Aarne Ranta	Syntactic Categories in the Language of Mathematics.	TYPES	1994	DBLP DOI BibTeX RDF
1	Amokrane Saïbi	Formalization of a lamda-Calculus with Explicit Substitutions in Coq.	TYPES	1994	DBLP DOI BibTeX RDF
1	Eduardo Giménez 0001	Codifying Guarded Definitions with Recursive Schemes.	TYPES	1994	DBLP DOI BibTeX RDF
1	Pascal Manoury	A User's Friendly Syntax to Define Recursive Functions as Typed lambda-Terms.	TYPES	1994	DBLP DOI BibTeX RDF
1	Susumu Hayashi	Logic of Refinement Types.	TYPES	1993	DBLP DOI BibTeX RDF
1	Herman Geuvers	Conservativity between Logics and Typed lambda Calculi.	TYPES	1993	DBLP DOI BibTeX RDF
1	Martin Hofmann 0001	Elimination of Extensionality in Martin-Löf Type Theory.	TYPES	1993	DBLP DOI BibTeX RDF
1	David A. Wolfram	Semantics for Abstract Clauses.	TYPES	1993	DBLP DOI BibTeX RDF
1	Thierry Coquand	Infinite Objects in Type Theory.	TYPES	1993	DBLP DOI BibTeX RDF
1	Leen Helmink, M. P. A. Sellink, Frits W. Vaandrager	Proof-Checking a Data Link Protocol.	TYPES	1993	DBLP DOI BibTeX RDF
1	Savi Maharaj	Encoding Z-style Schemas in Type Theory.	TYPES	1993	DBLP DOI BibTeX RDF
1	L. S. van Benthem Jutting, James McKinna, Robert Pollack	Checking Algorithms for Pure Type Systems.	TYPES	1993	DBLP DOI BibTeX RDF
1	Catherine Parent	Developing Certified Programs in the System Coq - The Program Tactic.	TYPES	1993	DBLP DOI BibTeX RDF
1	Randy Pollack	Closure Under Alpha-Conversion.	TYPES	1993	DBLP DOI BibTeX RDF
1	Marino Miculan	The Expressive Power of Structural Operational Semantics with Explicit Assumptions.	TYPES	1993	DBLP DOI BibTeX RDF
1	Thorsten Altenkirch	Proving Strong Normalization of CC by Modifying Realizability Semantics.	TYPES	1993	DBLP DOI BibTeX RDF
1	François Leclerc, Christine Paulin-Mohring	Programming with Streams in Coq - A Case Study: the Sieve of Eratosthenes.	TYPES	1993	DBLP DOI BibTeX RDF
1	Christophe Faffalli	Machine Deduction.	TYPES	1993	DBLP DOI BibTeX RDF
1	Aarne Ranta	Type Theory and the Informal Language of Mathematics.	TYPES	1993	DBLP DOI BibTeX RDF
1	Lena Magnusson, Bengt Nordström	The ALF Proof Editor and Its Proof Engine.	TYPES	1993	DBLP DOI BibTeX RDF

Publications at "TYPES"( http://dblp.L3S.de/Venues/TYPES )