Search results for "TYPES"

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

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