Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Robin Adams 0001 |
Formalized Metatheory with Terms Represented by an Indexed Family of Types. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Michel Parigot |
On Constructive Existence. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Yves Bertot, Benjamin Grégoire, Xavier Leroy |
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Meyer 0001, Burkhart Wolff |
Tactic-Based Optimized Compilation of Functional Programs. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli |
A Content Based Mathematical Search Engine: Whelp. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Claudio Sacerdoti Coen |
A Semi-reflexive Tactic for (Sub-)Equational Reasoning. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Stefano Berardi, Mario Coppo, Ferruccio Damiani (eds.) |
Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Adam Grabowski |
Solving Two Problems in General Topology Via Types. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Peter Morris, Thorsten Altenkirch, Conor McBride |
Exploring the Regular Tree Types. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Lionel Elie Mamane |
Surreal Numbers in Coq. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Ana Bove, Thierry Coquand |
Formalising Bitonic Sort in Type Theory. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Barthe, Sabrina Tarento |
A Machine-Checked Formalization of the Random Oracle Model. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Fredrik Lindblad, Marcin Benke |
A Tool for Automated Theorem Proving in Agda. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Conor McBride, Healfdene Goguen, James McKinna |
A Few Constructions on Constructors. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Alexandre Miquel |
lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Markus Michelbrink |
Interfaces as Games, Programs as Strategies. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Sergei Soloviev 0001, David Chemouil |
Some Algebraic Structures in Lambda-Calculus with Inductive Types. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Silvia Ghilezan, Pierre Lescanne |
Classical Proofs, Typed Processes, and Intersection Types: Extended Abstract. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Nicola Gambino, Martin Hyland |
Wellfounded Trees and Dependent Polynomial Functors. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Hongwei Xi |
Applied Type System: Extended Abstract. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Edwin C. Brady, Conor McBride, James McKinna |
Inductive Families Need Not Store Their Indices. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Sylvain Baro |
Introduction to PAF!, a Proof Assistant for ML Programs Verification. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Berghofer |
A Constructive Proof of Higman's Lemma in Isabelle. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Furio Honsell, Ivan Scagnetto |
Mobility Types in Coq. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Jacek Chrzaszcz |
Modules in Coq Are and Will Be Correct. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Horatiu Cirstea, Luigi Liquori, Benjamin Wack |
Rewriting Calculus with Fixpoints: Untyped and First-Order Systems. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
Rewriting-calculus, Object-calculus, Pattern Mat-ching, Lambda-calculus, Type Theory, Fixpoints |
1 | Clemens Ballarin |
Locales and Locale Expressions in Isabelle/Isar. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Freek Wiedijk |
Formal Proof Sketches. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Robin Adams 0001 |
A Modular Hierarchy of Logical Frameworks. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Viviana Bono, Jerzy Tiuryn, Pawel Urzyczyn |
Type Inference for Nested Self Types. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Fabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini |
Tailoring Filter Models. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Ugo Dal Lago, Simone Martini 0001, Luca Roversi |
Higher-Order Linear Ramified Recurrence. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Yong Luo 0001, Zhaohui Luo |
Combining Incoherent Coercions for Sigma-Types. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
1 | Herman Geuvers, Freek Wiedijk (eds.) |
Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Robert Kießling, Zhaohui Luo |
Coercions in Hindley-Milner Systems. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | José Espírito Santo, Luís Pinto 0001 |
Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Pierre Corbineau |
First-Order Reasoning in the Calculus of Inductive Constructions. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Milad Niqui, Yves Bertot |
QArith: Coq Formalisation of Lazy Rational Arithmetic. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Alberto Momigliano, Alwen Fernanto Tiu |
Induction and Co-induction in Sequent Calculus. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Lorenzo Bettini, Viviana Bono, Silvia Likavec |
A Core Calculus of Higher-Order Mixins and Classes. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker 0001 |
A Concurrent Logical Framework: The Propositional Fragment. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Michal Konecný |
Typing with Conditions and Guarantees for Functional In-place Update. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Yong Luo 0001, Zhaohui Luo, Sergei Soloviev 0001 |
Weak Transitivity in Coercive Subtyping. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Gueorgui I. Jojgov |
Holes with Binding Power. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Tarmo Uustalu |
Monad Translating Inductive and Coinductive Types. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Anton Setzer |
Java as a Functional Programming Language. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
object calculi, higher types, algebraic types, state pattern, Java, object-oriented programming, functional programming, Lambda calculus, visitor pattern, initial algebras, call-by-value |
1 | 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 |
1 | Laurent Chicli, Loic Pottier, Carlos Simpson |
Mathematical Quotients and Quotient Types in Coq. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Pietro Di Gianantonio, Marino Miculan |
A Unifying Approach to Recursive and Co-recursive Definitions. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Tobias Nipkow |
Structured Proofs in Isar/HOL. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Pierre Letouzey |
A New Extraction for Coq. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Alexandre Miquel, Benjamin Werner |
The Not So Simple Proof-Irrelevant Model of CC. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Stéphane Vaillant |
A Finite First-Order Presentation of Set Theory. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Luís Cruz-Filipe |
A Constructive Formalization of the Fundamental Theorem of Calculus. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Jesper Carlström |
Subsets, Quotients and Partial Functions in Martin-Löf's Type Theory. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Abel 0001, Ralph Matthes |
(Co-)Iteration for Higher-Order Nested Datatypes. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Mariangiola Dezani-Ciancaglini, Silvia Ghilezan |
Two Behavioural Lambda Models. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Berghofer |
Program Extraction in Simply-Typed Higher Order Logic. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Ana Bove |
General Recursion in Type Theory. |
TYPES |
2002 |
DBLP DOI BibTeX RDF |
|
1 | Herman Geuvers, Milad Niqui |
Constructive Reals in Coq: Axioms and Categoricity. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Kristofer Johannisson |
Formalizing the Halting Problem in a Constructive Type Theory. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Matt Fairtlough, Michael Mendler |
On the Logical Content of Computational Type Theory: A Solution to Curry's Problem. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Peter Aczel, Nicola Gambino |
Collection Principles in Dependent Type Theory. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Nicolas Magaud, Yves Bertot |
Changing Data Structures in Type Theory: A Study of Natural Numbers. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Susumu Hayashi, Masahiro Nakata |
Towards Limit Computable Mathematics. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Conor McBride |
Elimination with a Motive. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Coquand, Makoto Takeyama |
An Implementation of Type: Type. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Berghofer, Tobias Nipkow |
Executing Higher Order Logic. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Healfdene Goguen |
A Kripke-Style Model for the Admissibility of Structural Rules. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Pons |
Generalization in Type Theory Based Proof Assistants. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Giuseppe Longo |
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Monika Seisenberger |
An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Alberto Ciaffaglione, Pietro Di Gianantonio |
A Tour with Constructive Real Numbers. |
TYPES |
2000 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Gustavo Betarte, Cristina Cornes, Nora Szasz, Alvaro Tasistro |
Specification of a Smart Card Operating System. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Micaela Mayero |
The Three Gap Theorem (Steinhaus Conjecture). |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Abel 0001 |
Specification and Verification of a Formal System for Structurally Recursive Functions. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | David Delahaye |
Information Retrieval in a Coq Proof Library Using Type Isomorphisms. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Steffen van Bakel, Franco Barbanera, Maribel Fernández |
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstractions and beta-Rule. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Qiao Haiyan |
Formalising Formulas-as-Types-as-Objects. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Abel 0001, Thorsten Altenkirch |
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Alberto Ciaffaglione, Pietro Di Gianantonio |
A Co-inductive Approach to Real Numbers. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Paul Callaghan, Zhaohui Luo |
Implementation Techniques for Inductive Types in Plastic. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
inductive types, LF implementation, type theory |
1 | Healfdene Goguen, Richard Brooksby, Rod M. Burstall |
Memory Management: An Abstract Formulation of Incremental Tracing. |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Gertrud Bauer, Markus Wenzel 0001 |
Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar). |
TYPES |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Christophe Filliâtre |
Proof of Imperative Programs in Type Theory. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Frank Pfenning, Carsten Schürmann |
Algorithms for Equality and Unification in the Presence of Notational Definitions. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Kleymann |
Metatheory of Verification Calculi in LEGO - To what Extent Does Syntax Matter? |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | René M. C. Ahn, Tijn Borghuis |
Communication Modelling and Context-Dependent Interpretation: An Integrated Approach. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Maria Emilia Maietti |
About Effective Quotients in Constructive Type Theory. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Giovanni Sambin, Silvia Gebellato |
A Preview of the Basic Picture: A New Perspective on Formal Topology. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Luigi Liquori |
Bounded Polymorphism for Extensible Objects. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Jean Goubault-Larrecq |
Conjunctive Types and SKInT. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Florian Kammüller |
Modular Structures as Dependent Types in Isabelle. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Dowek, Benjamin Werner |
Proof Normalization Modulo. |
TYPES |
1998 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|