Search results for "types"

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