Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
32 | Fabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini |
Tailoring Filter Models. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
32 | Furio Honsell, Marina Lenisa |
"Wave-Style" Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
(linear) graph model, traced monoidal category, weak linear category, categorical geometry of interaction |
32 | Robert Kießling, Zhaohui Luo |
Coercions in Hindley-Milner Systems. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
32 | José Espírito Santo, Luís Pinto 0001 |
Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
32 | Pierre Corbineau |
First-Order Reasoning in the Calculus of Inductive Constructions. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
32 | Milad Niqui, Yves Bertot |
QArith: Coq Formalisation of Lazy Rational Arithmetic. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
32 | Alberto Momigliano, Alwen Fernanto Tiu |
Induction and Co-induction in Sequent Calculus. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
32 | Lorenzo Bettini, Viviana Bono, Silvia Likavec |
A Core Calculus of Higher-Order Mixins and Classes. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
32 | Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack (eds.) |
Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Michal Konecný |
Typing with Conditions and Guarantees for Functional In-place Update. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Achim D. Brucker, Burkhart Wolff |
Using Theory Morphisms for Implementing Formal Methods Tools. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
Shallow Embeddings, Formal Methods, Theorem Proving, OCL, Formal Semantics |
32 | Pietro Di Gianantonio, Marino Miculan |
A Unifying Approach to Recursive and Co-recursive Definitions. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Tobias Nipkow |
Structured Proofs in Isar/HOL. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Pierre Letouzey |
A New Extraction for Coq. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Alexandre Miquel, Benjamin Werner |
The Not So Simple Proof-Irrelevant Model of CC. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Stéphane Vaillant |
A Finite First-Order Presentation of Set Theory. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Luís Cruz-Filipe |
A Constructive Formalization of the Fundamental Theorem of Calculus. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Jesper Carlström |
Subsets, Quotients and Partial Functions in Martin-Löf's Type Theory. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Mariangiola Dezani-Ciancaglini, Silvia Ghilezan |
Two Behavioural Lambda Models. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Stefan Berghofer |
Program Extraction in Simply-Typed Higher Order Logic. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Ana Bove |
General Recursion in Type Theory. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith (eds.) |
Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | David Walker 0001, J. Gregory Morrisett |
Alias Types for Recursive Data Structures. |
Types in Compilation |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Herman Geuvers, Milad Niqui |
Constructive Reals in Coq: Axioms and Categoricity. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Kristofer Johannisson |
Formalizing the Halting Problem in a Constructive Type Theory. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Matt Fairtlough, Michael Mendler |
On the Logical Content of Computational Type Theory: A Solution to Curry's Problem. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Peter Aczel, Nicola Gambino |
Collection Principles in Dependent Type Theory. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Nicolas Magaud, Yves Bertot |
Changing Data Structures in Type Theory: A Study of Natural Numbers. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Susumu Hayashi, Masahiro Nakata |
Towards Limit Computable Mathematics. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Herman Geuvers, Freek Wiedijk, Jan Zwanenburg |
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Conor McBride |
Elimination with a Motive. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Stefan Berghofer, Tobias Nipkow |
Executing Higher Order Logic. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Healfdene Goguen |
A Kripke-Style Model for the Admissibility of Structural Rules. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Olivier Pons |
Generalization in Type Theory Based Proof Assistants. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Giuseppe Longo |
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Monika Seisenberger |
An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Alberto Ciaffaglione, Pietro Di Gianantonio |
A Tour with Constructive Real Numbers. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Thorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus (eds.) |
Types for Proofs and Programs, International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
32 | Gustavo Betarte, Cristina Cornes, Nora Szasz, Alvaro Tasistro |
Specification of a Smart Card Operating System. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
32 | Micaela Mayero |
The Three Gap Theorem (Steinhaus Conjecture). |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
32 | David Delahaye |
Information Retrieval in a Coq Proof Library Using Type Isomorphisms. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
32 | Healfdene Goguen, Richard Brooksby, Rod M. Burstall |
Memory Management: An Abstract Formulation of Incremental Tracing. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
32 | Gertrud Bauer, Markus Wenzel 0001 |
Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar). |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
32 | Eduardo Giménez 0001, Christine Paulin-Mohring (eds.) |
Types for Proofs and Programs, International Workshop TYPES'96, Aussois, France, December 15-19, 1996, Selected Papers |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Andrew P. Tolmach |
Optimizing ML Using a Hierarchy of Monadic Types. |
Types in Compilation |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Jean-Christophe Filliâtre |
Proof of Imperative Programs in Type Theory. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Frank Pfenning, Carsten Schürmann |
Algorithms for Equality and Unification in the Presence of Notational Definitions. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Thomas Kleymann |
Metatheory of Verification Calculi in LEGO - To what Extent Does Syntax Matter? |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | René M. C. Ahn, Tijn Borghuis |
Communication Modelling and Context-Dependent Interpretation: An Integrated Approach. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Maria Emilia Maietti |
About Effective Quotients in Constructive Type Theory. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Giovanni Sambin, Silvia Gebellato |
A Preview of the Basic Picture: A New Perspective on Formal Topology. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Luigi Liquori |
Bounded Polymorphism for Extensible Objects. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Gilles Dowek, Benjamin Werner |
Proof Normalization Modulo. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | Daniel Fridlender |
An Interpretation of the Fan Theorem in Type Theory. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
fan theorem, inductive bar, type theory |
32 | Thierry Coquand, Henrik Persson |
Gröbner Bases in Type Theory. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
32 | 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 |
|
32 | Conor McBride |
Inverting Inductively Defined Relations in LEGO. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Sara Negri |
Continous Lattices in Formal Topology. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Daniel Fridlender |
Highman's Lemma in theory. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Anthony Bailey |
Coercion Synthesis in Computer Implementations of Type-Theoretic Frameworks. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Jean Goubault-Larrecq |
A Proof of Weak Termination of Typed lambda-sigma-Calculi. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Jan Cederquist |
An Implementation of the Heine-Borel Covering Theorem in Type Theory. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Petri Mäenpää |
Semantical BNF. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | John Harrison 0001 |
Proof Style. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Wolfgang Naraschewski, Tobias Nipkow |
Type Inference Verified: Algorithm W in Isabelle/HOL. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Maria Emilia Maietti |
The Internal Type Theory of a Heyting Pretopos. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Ferruccio Damiani, Frédéric Prost |
Detecting and Removing Dead-Code using Rank 2 Intersection. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Bruno Barras |
Verification of the Interface of a Small Proof System in Coq. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Eduardo Giménez 0001, Christine Paulin-Mohring |
Introduction. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Paul-André Melliès, Benjamin Werner |
A Generic Normalisation Proof for Pure Type Systems. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Gilles Dowek |
A Type-Free Formalization of Mathematics where Proofs are Objects. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Jean-François Monin |
Proving a Real Time Algorithm for ATM in Coq. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | Alex P. Jones, Zhaohui Luo, Sergei Soloviev 0001 |
Some Algorithmic and Proof-Theoretical Aspects of Coercive Subtyping. |
TYPES |
1996 |
DBLP DOI BibTeX RDF |
|
32 | 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 |
|
32 | Tanel Tammet, Jan M. Smith |
Optimized Encodings of Fragments of Type Theory in First Order Logic. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | Cristina Cornes, Delphine Terrasse |
Automating Inversion of Inductive Predicates in Coq. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | Jan Cederquist, Sara Negri |
A Constructive Proof of the Heine-Borel Covering Theorem for Formal Reals. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | 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 |
|
32 | Furio Honsell, Marino Miculan |
A Natural Deduction Approach to Dynamic Logic. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | Aarne Ranta |
Context-Relative Syntactic Categories and the Formalization of Mathematical Text. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | Milena Stefanova, Herman Geuvers |
A Simple Model Construction for the Calculus of Constructions. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | Jan von Plato |
Organization and Development of a Constructive Axiomatization. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | Lena Magnusson |
An Algorithm for Checking Incomplete Proof Objects in Type Theory with Localization and Unification. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | Ulrich Berger 0001, Helmut Schwichtenberg |
The Greatest Common Divisor: A Case Study for Program Extraction from Classical Proofs. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | Thierry Coquand, Jan M. Smith |
An Application of Constructive Completeness. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
32 | 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 |
|
32 | René M. C. Ahn |
Communication Contexts: a Pragmatic Approach to Information Exchange. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Herman Geuvers |
A short and flexible proof of Strong Normalization for the Calculus of Constructions. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Robert Pollack |
On Extensibility of Proof Checkers. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Lawrence C. Paulson |
A Concrete Final Coalgebra Theorem for ZF Set Theory. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Healfdene Goguen |
The Metatheory of UTT. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Tobias Nipkow, Konrad Slind |
I/Q Automata in Isabelle/HOL. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Aarne Ranta |
Syntactic Categories in the Language of Mathematics. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Amokrane Saïbi |
Formalization of a lamda-Calculus with Explicit Substitutions in Coq. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Eduardo Giménez 0001 |
Codifying Guarded Definitions with Recursive Schemes. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Pascal Manoury |
A User's Friendly Syntax to Define Recursive Functions as Typed lambda-Terms. |
TYPES |
1994 |
DBLP DOI BibTeX RDF |
|
32 | Herman Geuvers |
Conservativity between Logics and Typed lambda Calculi. |
TYPES |
1993 |
DBLP DOI BibTeX RDF |
|
32 | Martin Hofmann 0001 |
Elimination of Extensionality in Martin-Löf Type Theory. |
TYPES |
1993 |
DBLP DOI BibTeX RDF |
|
32 | David A. Wolfram |
Semantics for Abstract Clauses. |
TYPES |
1993 |
DBLP DOI BibTeX RDF |
|
32 | Thierry Coquand |
Infinite Objects in Type Theory. |
TYPES |
1993 |
DBLP DOI BibTeX RDF |
|