Search results for "coq"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
11	Carsten Schürmann	Twelf and Delphin: Logic and Functional Programming in a Meta-logical Framework.	FLOPS	2004	DBLP DOI BibTeX RDF
11	Luigi Liquori, Bernard P. Serpette	iRho: an imperative rewriting calculus.	PPDP	2004	DBLP DOI BibTeX RDF	certied software, rewriting-calculus, pattern-matching, types, term rewriting systems, natural semantics
11	Gilles Barthe, Guillaume Dufay	A Tool-Assisted Framework for Certified Bytecode Verification.	FASE	2004	DBLP DOI BibTeX RDF
11	Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni	A Syntactic Approach to Foundational Proof-Carrying Code.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	foundational proof-carrying code, syntactic soundness proof, typed assembly language
11	Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin	Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures.	ICFEM	2003	DBLP DOI BibTeX RDF
11	Luís Cruz-Filipe, Bas Spitters	Program Extraction from Large Proof Developments.	TPHOLs	2003	DBLP DOI BibTeX RDF
11	Laurent Théry	Proving Pearl: Knuth's Algorithm for Prime Numbers.	TPHOLs	2003	DBLP DOI BibTeX RDF
11	Frédéric Blanqui	Inductive Types in the Calculus of Algebraic Constructions.	TLCA	2003	DBLP DOI BibTeX RDF
11	Thierry Coquand, Randy Pollack, Makoto Takeyama	A Logical Framework with Dependently Typed Records.	TLCA	2003	DBLP DOI BibTeX RDF
11	Sylvie Boldo, Marc Daumas	Representable Correcting Terms for Possibly Underflowing Floating Point Operations.	IEEE Symposium on Computer Arithmetic	2003	DBLP DOI BibTeX RDF
11	Pierre Corbineau	First-Order Reasoning in the Calculus of Inductive Constructions.	TYPES	2003	DBLP DOI BibTeX RDF
11	Alberto Ciaffaglione, Luigi Liquori, Marino Miculan	Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax.	MERLIN	2003	DBLP DOI BibTeX RDF	logical foundations of programming, object-based calculi with side-effects, program and system verification, logical frameworks, interactive theorem proving
11	Claudio Sacerdoti Coen	A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics.	ICTCS	2003	DBLP DOI BibTeX RDF
11	Dimitri Hendriks, Vincent van Oostrom	adbmal	CADE	2003	DBLP DOI BibTeX RDF
11	Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen 0002	Proof Search and Proof Check for Equational and Inductive Theorems.	CADE	2003	DBLP DOI BibTeX RDF	proof terms, computation, induction, automated theorem proving, deduction, rewrite rules, proof assistant
11	Claudio Sacerdoti Coen	From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls.	MKM	2003	DBLP DOI BibTeX RDF
11	Judicaël Courant	Explicit Universes for the Calculus of Constructions.	TPHOLs	2002	DBLP DOI BibTeX RDF
11	Virgile Prevosto, Damien Doligez, Thérèse Hardin	Algebraic Structures and Dependent Records.	TPHOLs	2002	DBLP DOI BibTeX RDF
11	Christophe Dehlinger, Jean-François Dufourd	Formalizing the Trading Theorem for the Classification of Surfaces.	TPHOLs	2002	DBLP DOI BibTeX RDF
11	Luc Moreau 0001	A fault-tolerant directory service for mobile agents based on forwarding pointers.	SAC	2002	DBLP DOI BibTeX RDF	distributed directory service, fault tolerance, mobile agents
11	Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni	A Syntactic Approach to Foundational Proof-Carrying Code.	LICS	2002	DBLP DOI BibTeX RDF
11	Pietro Di Gianantonio, Marino Miculan	A Unifying Approach to Recursive and Co-recursive Definitions.	TYPES	2002	DBLP DOI BibTeX RDF
11	Luís Cruz-Filipe	A Constructive Formalization of the Fundamental Theorem of Calculus.	TYPES	2002	DBLP DOI BibTeX RDF
11	Robert R. Schneck, George C. Necula	A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code.	CADE	2002	DBLP DOI BibTeX RDF
11	Jean-Paul Bodeveix, Mamoun Filali	Type Synthesis in B and the Translation of B to PVS.	ZB	2002	DBLP DOI BibTeX RDF	semantics, type theory, PVS, logical frameworks, B
11	Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa	A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines.	VMCAI	2002	DBLP DOI BibTeX RDF
11	Luc Moreau 0001, Jean Duprat	A construction of distributed reference counting.	Acta Informatica	2001	DBLP DOI BibTeX RDF
11	Marc Daumas, Laurence Rideau, Laurent Théry	A Generic Library for Floating-Point Numbers and Its Application to Exact Computing.	TPHOLs	2001	DBLP DOI BibTeX RDF
11	Christine Röckl, Daniel Hirschkoff, Stefan Berghofer	Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts.	FoSSaCS	2001	DBLP DOI BibTeX RDF
11	Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard P. Serpette, Simão Melo de Sousa	A Formal Executable Semantics of the JavaCard Platform.	ESOP	2001	DBLP DOI BibTeX RDF
11	Marko Luther	More On Implicit Syntax.	IJCAR	2001	DBLP DOI BibTeX RDF
11	Benjamin C. Pierce, Jerome Vouillon	Unison: A File Synchronizer and Its Specification.	TACS	2001	DBLP DOI BibTeX RDF
11	Pierre Courtieu	Normalized Types.	CSL	2001	DBLP DOI BibTeX RDF
11	Christophe Dehlinger, Jean-François Dufourd, Pascal Schreck	Higher-Order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry.	Automated Deduction in Geometry	2000	DBLP DOI BibTeX RDF
11	Herman Geuvers, Freek Wiedijk, Jan Zwanenburg	Equational Reasoning via Partial Reflection.	TPHOLs	2000	DBLP DOI BibTeX RDF
11	Antonia Balaa, Yves Bertot	Fix-Point Equations for Well-Founded Recursion in Type Theory.	TPHOLs	2000	DBLP DOI BibTeX RDF
11	Venanzio Capretta	Recursive Families of Inductive Types.	TPHOLs	2000	DBLP DOI BibTeX RDF
11	Gilles Barthe, Femke van Raamsdonk	Constructor Subtyping in the Calculus of Inductive Constructions.	FoSSaCS	2000	DBLP DOI BibTeX RDF
11	Ewen Denney, Thomas P. Jensen	Correctness of Java Card Method Lookup via Logical Relations.	ESOP	2000	DBLP DOI BibTeX RDF
11	Nicolas Magaud, Yves Bertot	Changing Data Structures in Type Theory: A Study of Natural Numbers.	TYPES	2000	DBLP DOI BibTeX RDF
11	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
11	Conor McBride	Elimination with a Motive.	TYPES	2000	DBLP DOI BibTeX RDF
11	David Aspinall 0001	Proof General: A Generic Tool for Proof Development.	TACAS	2000	DBLP DOI BibTeX RDF
11	Florian Kammüller, Markus Wenzel 0001, Lawrence C. Paulson	Locales - A Sectioning Concept for Isabelle.	TPHOLs	1999	DBLP DOI BibTeX RDF
11	Venanzio Capretta	Universal Algebra in Type Theory.	TPHOLs	1999	DBLP DOI BibTeX RDF
11	Marino Miculan	Formalizing a Lazy Substitution Proof System for µ-calculus in the Calculus of Inductive Constructions.	ICALP	1999	DBLP DOI BibTeX RDF
11	Gustavo Betarte, Cristina Cornes, Nora Szasz, Alvaro Tasistro	Specification of a Smart Card Operating System.	TYPES	1999	DBLP DOI BibTeX RDF
11	Micaela Mayero	The Three Gap Theorem (Steinhaus Conjecture).	TYPES	1999	DBLP DOI BibTeX RDF
11	Alberto Ciaffaglione, Pietro Di Gianantonio	A Co-inductive Approach to Real Numbers.	TYPES	1999	DBLP DOI BibTeX RDF
11	Healfdene Goguen, Richard Brooksby, Rod M. Burstall	Memory Management: An Abstract Formulation of Incremental Tracing.	TYPES	1999	DBLP DOI BibTeX RDF
11	François Puitg, Jean-François Dufourd	Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling.	TPHOLs	1998	DBLP DOI BibTeX RDF
11	David Nowak, Jean-René Beauvais, Jean-Pierre Talpin	Co-inductive Axiomatization of a Synchronous Language.	TPHOLs	1998	DBLP DOI BibTeX RDF
11	François Puitg, Jean-François Dufourd	Formal Program Development in Geometric Modeling.	FM-Trends	1998	DBLP DOI BibTeX RDF
11	Jean-Christophe Filliâtre	Proof of Imperative Programs in Type Theory.	TYPES	1998	DBLP DOI BibTeX RDF
11	Frank Pfenning, Carsten Schürmann	Algorithms for Equality and Unification in the Presence of Notational Definitions.	TYPES	1998	DBLP DOI BibTeX RDF
11	Peter Aczel	On Relating Type Theories and Set Theories.	TYPES	1998	DBLP DOI BibTeX RDF
11	Daniel Hirschkoff	A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions.	TPHOLs	1997	DBLP DOI BibTeX RDF
11	Gang Chen	Subtyping Calculus of Construction (Extended Abstract).	MFCS	1997	DBLP DOI BibTeX RDF
11	Janet Bertot, Yves Bertot	CtCoq: A System Presentation.	CADE	1996	DBLP DOI BibTeX RDF	system presentation, Application