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 |
|