Search results for "coq"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
16	Iman Poernomo, Jeffrey Terrell	Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq.	ICFEM	2010	DBLP DOI BibTeX RDF
16	Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi	Program Calculation in Coq.	AMAST	2010	DBLP DOI BibTeX RDF
16	José Bacelar Almeida, Nelma Moreira, David Pereira, Simão Melo de Sousa	Partial Derivative Automata Formalized in Coq.	CIAA	2010	DBLP DOI BibTeX RDF
16	Adam Chlipala	Foundational Program Verification in Coq with Automated Proofs.	MSFP@ICFP	2010	DBLP DOI BibTeX RDF
16	Amy P. Felty	Hybrid: Reasoning with Higher-Order Abstract Syntax in Coq and Isabelle.	MSFP@ICFP	2010	DBLP DOI BibTeX RDF
16	Martin Hofmann 0001, Aleksandr Karbyshev, Helmut Seidl	Verifying a Local Generic Solver in Coq.	SAS	2010	DBLP DOI BibTeX RDF
16	Chantal Keller, Benjamin Werner	Importing HOL Light into Coq.	ITP	2010	DBLP DOI BibTeX RDF
16	Bas Spitters, Eelis van der Weegen	Developing the Algebraic Hierarchy with Type Classes in Coq.	ITP	2010	DBLP DOI BibTeX RDF
16	Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry	Extending Coq with Imperative Features and Its Application to SAT Verification.	ITP	2010	DBLP DOI BibTeX RDF
16	Thomas Braibant, Damien Pous	An Efficient Coq Tactic for Deciding Kleene Algebras.	ITP	2010	DBLP DOI BibTeX RDF
16	Pierre-Yves Strub	Coq Modulo Theory.	CSL	2010	DBLP DOI BibTeX RDF
16	Maciej Piróg, Dariusz Biernacki	A systematic derivation of the STG machine verified in Coq.	Haskell	2010	DBLP DOI BibTeX RDF
16	César Domínguez 0001, Julio Rubio 0001	Computing in Coq with Infinite Algebraic Data Structures.	AISC/MKM/Calculemus	2010	DBLP DOI BibTeX RDF
16	Hai Wan, Xiaoyu Song, Ming Gu 0001	Parameterized Specification and Verification of PLC Systems in Coq.	TASE	2010	DBLP DOI BibTeX RDF
16	Adam Koprowski	Coq formalization of the higher-order recursive path ordering.	Appl. Algebra Eng. Commun. Comput.	2009	DBLP DOI BibTeX RDF
16	Philippe Audebaud, Christine Paulin-Mohring	Proofs of randomized algorithms in Coq.	Sci. Comput. Program.	2009	DBLP DOI BibTeX RDF
16	Wendy Verbruggen, Edsko de Vries, Arthur Hughes	Polytypic properties and proofs in Coq.	WGP@ICFP	2009	DBLP DOI BibTeX RDF
16	Daniel W. H. James, Ralf Hinze	A Reflection-based Proof Tactic for Lattices in Coq.	Trends in Functional Programming	2009	DBLP BibTeX RDF
16	Christine Choppy, Micaela Mayero, Laure Petrucci	Coloured Petri net refinement specification, and correctness proof with Coq.	NASA Formal Methods	2009	DBLP BibTeX RDF
16	Yves Bertot, Ekaterina Komendantskaya	Inductive and Coinductive Components of Corecursive Functions in Coq.	CMCS	2008	DBLP DOI BibTeX RDF
16	David Pereira, Nelma Moreira	KAT and PHL in Coq.	Comput. Sci. Inf. Syst.	2008	DBLP DOI BibTeX RDF
16	Concepción Vidal, Felicidad Aguado, José Luis Doncel, José María Molinelli, Gilberto Pérez 0001	Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator.	J. Formaliz. Reason.	2008	DBLP DOI BibTeX RDF
16	Yves Bertot, Ekaterina Komendantskaya	Inductive and Coinductive Components of Corecursive Functions in Coq	CoRR	2008	DBLP BibTeX RDF
16	Jean-François Dufourd	Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps	CoRR	2008	DBLP BibTeX RDF
16	Yves Bertot	Structural abstract interpretation, A formal study using Coq	CoRR	2008	DBLP BibTeX RDF
16	Russell O'Connor	Certified Exact Transcendental Real Number Computation in Coq	CoRR	2008	DBLP BibTeX RDF
16	Nicolas Magaud, Julien Narboux, Pascal Schreck	Formalizing Projective Plane Geometry in Coq.	Automated Deduction in Geometry	2008	DBLP DOI BibTeX RDF
16	Loic Pottier	Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics.	LPAR Workshops	2008	DBLP BibTeX RDF
16	Jean-François Dufourd	Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps.	STACS	2008	DBLP DOI BibTeX RDF
16	Yves Bertot, Vladimir Komendantsky	Fixed point semantics and partial recursion in Coq.	PPDP	2008	DBLP DOI BibTeX RDF	least fixed point semantics, non-terminating functions, program extraction, the Knaster-Tarski theorem, automated theorem proving
16	Assia Mahboubi	Implementing the cylindrical algebraic decomposition within the Coq system.	Math. Struct. Comput. Sci.	2007	DBLP DOI BibTeX RDF
16	Houda Anoun	Une bibliothèque Coq pour le traitement des langues naturelles.	Tech. Sci. Informatiques	2007	DBLP DOI BibTeX RDF
16	Matthieu Sozeau	Program-ing finger trees in Coq.	ICFP	2007	DBLP DOI BibTeX RDF
16	Brian E. Aydemir, Aaron Bohannon, Stephanie Weirich	Nominal Reasoning Techniques in Coq: (Extended Abstract).	LFMTP@FLoC	2006	DBLP DOI BibTeX RDF
16	Yves Bertot	Coq in a Hurry	CoRR	2006	DBLP BibTeX RDF
16	Laurent Théry	Formalising Sylow's theorems in Coq	CoRR	2006	DBLP BibTeX RDF
16	Yves Bertot	CoInduction in Coq	CoRR	2006	DBLP BibTeX RDF
16	Laurent Théry, Pierre Letouzey, Georges Gonthier	Coq.	The Seventeen Provers of the World	2006	DBLP DOI BibTeX RDF
16	Jacek Chrzaszcz, Jean-Pierre Jouannaud	From OBJ to ML to Coq.	Essays Dedicated to Joseph A. Goguen	2006	DBLP DOI BibTeX RDF
16	Jean-Pierre Jouannaud, Weiwen Xu	Automatic Complexity Analysis for Programs Extracted from Coq Proof.	CLASE	2005	DBLP DOI BibTeX RDF
16	Frédérique Guilhot	Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée.	Tech. Sci. Informatiques	2005	DBLP DOI BibTeX RDF
16	David Delahaye, Mathieu Jaume, Virgile Prevosto	Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs.	Tech. Sci. Informatiques	2005	DBLP DOI BibTeX RDF
16	David Delahaye, Micaela Mayero	Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant	CoRR	2005	DBLP BibTeX RDF
16	Russell O'Connor	Essential Incompleteness of Arithmetic Verified by Coq	CoRR	2005	DBLP BibTeX RDF
16	David Delahaye, Micaela Mayero	Dealing with algebraic expressions over a field in Coq using Maple.	J. Symb. Comput.	2005	DBLP DOI BibTeX RDF
16	Assia Mahboubi	Programming and certifying a CAD algorithm in the Coq system.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
16	Reynald Affeldt, Naoki Kobayashi 0001	A Coq Library for Verification of Concurrent Programs.	LFM@IJCAR	2004	DBLP DOI BibTeX RDF
16	Christophe Dehlinger, Jean-François Dufourd	Formalizing the trading theorem in Coq.	Theor. Comput. Sci.	2004	DBLP DOI BibTeX RDF
16	Christophe Dehlinger, Jean-François Dufourd	Formalizing generalized maps in Coq.	Theor. Comput. Sci.	2004	DBLP DOI BibTeX RDF
16	Yves Bertot, Pierre Castéran	Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions		2004	DOI RDF
16	Christelle Brèque	Micro-environnement des spermatozoides de coq dans les glandes utéro-vaginales: applications au contrôle de la fertilité.		2004	RDF
16	Martijn Oostdijk, Herman Geuvers	Proof by computation in the Coq system.	Theor. Comput. Sci.	2002	DBLP DOI BibTeX RDF
16	Dimitri Hendriks	Proof Reflection in Coq.	J. Autom. Reason.	2002	DBLP DOI BibTeX RDF
16	Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg	A Constructive Algebraic Hierarchy in Coq.	J. Symb. Comput.	2002	DBLP DOI BibTeX RDF
16	Nicolas Magaud, Yves Bertot	Changement de représentation des structures de données en Coq: le cas des entiers naturels.	JFLA	2001	DBLP BibTeX RDF
16	David Delahaye, Micaela Mayero	Field, une procédure de décision pour les nombres réels en Coq.	JFLA	2001	DBLP BibTeX RDF
16	Laurent Chicli	Une formalisation des faisceaux et des schémas affines en théorie des types avec Coq.	JFLA	2001	DBLP BibTeX RDF
16	Pierre Letouzey, Laurent Théry	Formalizing Stålmarck's Algorithm in Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF
16	Catherine Dubois, Valérie Ménissier-Morain	Certification of a Type Inference Tool for ML: Damas-Milner within Coq.	J. Autom. Reason.	1999	DBLP DOI BibTeX RDF
16	Kok Meng Yew, M. Zahidur Rahman, Sai Peck Lee	Formal Verification of Secret Sharing Protocol Using Coq.	ASIAN	1999	DBLP DOI BibTeX RDF
16	Barbara Heyd, Pierre Crégut	A Modular Coding of UNITY in COQ.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Solange Coupet-Grimal, Line Jakubiec	Coq and Hardware Verification: A Case Study.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Bruno Barras	Verification of the Interface of a Small Proof System in Coq.	TYPES	1996	DBLP DOI BibTeX RDF
16	Jean-François Monin	Proving a Real Time Algorithm for ATM in Coq.	TYPES	1996	DBLP DOI BibTeX RDF
16	Delphine Terrasse	Encoding Natural Semantics in Coq.	AMAST	1995	DBLP DOI BibTeX RDF
16	François Leclerc	Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coq.	TLCA	1995	DBLP DOI BibTeX RDF
16	Joëlle Despeyroux, Amy P. Felty, André Hirschowitz	Higher-Order Abstract Syntax in Coq.	TLCA	1995	DBLP DOI BibTeX RDF
16	Cristina Cornes, Delphine Terrasse	Automating Inversion of Inductive Predicates in Coq.	TYPES	1995	DBLP DOI BibTeX RDF
16	Eduardo Giménez 0001	An Application of Co-inductive Types in Coq: Verification of the Alternating Bit Protocol.	TYPES	1995	DBLP DOI BibTeX RDF
16	Amokrane Saïbi	Formalization of a lamda-Calculus with Explicit Substitutions in Coq.	TYPES	1994	DBLP DOI BibTeX RDF
16	Christine Paulin-Mohring, Benjamin Werner	Synthesis of ML Programs in the System Coq.	J. Symb. Comput.	1993	DBLP DOI BibTeX RDF
16	Christine Paulin-Mohring	Inductive Definitions in the system Coq - Rules and Properties.	TLCA	1993	DBLP DOI BibTeX RDF
16	Catherine Parent	Developing Certified Programs in the System Coq - The Program Tactic.	TYPES	1993	DBLP DOI BibTeX RDF
16	François Leclerc, Christine Paulin-Mohring	Programming with Streams in Coq - A Case Study: the Sieve of Eratosthenes.	TYPES	1993	DBLP DOI BibTeX RDF
11	Limin Jia 0001, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich	Dependent types and program equivalence.	POPL	2010	DBLP DOI BibTeX RDF	dependent types, program equivalence
11	Aquinas Hobor, Robert Dockins, Andrew W. Appel	A theory of indirection via approximation.	POPL	2010	DBLP DOI BibTeX RDF	indirection theory, step-indexed models
11	Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine	Structuring the verification of heap-manipulating programs.	POPL	2010	DBLP DOI BibTeX RDF	type theory, monads, hoare logic, separation logic
11	Andreas Rossberg, Claudio V. Russo, Derek Dreyer	F-ing modules.	TLDI	2010	DBLP DOI BibTeX RDF	first-class modules, ml modules, type systems, abstract data types, system f, existential types, elaboration
11	Sylvie Boldo	Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven.	IEEE Trans. Computers	2009	DBLP DOI BibTeX RDF
11	Xavier Leroy	Formal verification of a realistic compiler.	Commun. ACM	2009	DBLP DOI BibTeX RDF
11	Hugo Herbelin, Gyesik Lee	Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus.	WoLLIC	2009	DBLP DOI BibTeX RDF	Intuitionistic Gentzen-style sequent calculus, completeness, cut-elimination, Kripke semantics
11	Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet	Implementing a Direct Method for Certificate Translation.	ICFEM	2009	DBLP DOI BibTeX RDF
11	Keiko Nakata 0001, Tarmo Uustalu	Trace-Based Coinductive Operational Semantics for While.	TPHOLs	2009	DBLP DOI BibTeX RDF
11	Wouter Swierstra	A Hoare Logic for the State Monad.	TPHOLs	2009	DBLP DOI BibTeX RDF
11	Frédéric Dabrowski, David Pichardie	A Certified Data Race Analysis for a Java-like Language.	TPHOLs	2009	DBLP DOI BibTeX RDF
11	Nicolas Julien, Ioana Pasca	Formal Verification of Exact Computations Using Newton's Method.	TPHOLs	2009	DBLP DOI BibTeX RDF
11	Andrew McCreight	Practical Tactics for Separation Logic.	TPHOLs	2009	DBLP DOI BibTeX RDF
11	Robert Atkey	Syntax for Free: Representing Syntax with Binding Using Parametricity.	TLCA	2009	DBLP DOI BibTeX RDF
11	Yuan Dong, Kai Ren, Shengyuan Wang, Suqin Zhang	Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine.	APLAS	2009	DBLP DOI BibTeX RDF
11	Robert Dockins, Aquinas Hobor, Andrew W. Appel	A Fresh Look at Separation Algebras and Share Accounting.	APLAS	2009	DBLP DOI BibTeX RDF
11	Richard Dapoigny, Patrick Barlatier	Towards an Ontological Modeling with Dependent Types: Application to Part-Whole Relations.	ER	2009	DBLP DOI BibTeX RDF
11	Yuan Dong, Shengyuan Wang, Liwei Zhang, Ping Yang	Modular Certification of Low-Level Intermediate Representation Programs.	COMPSAC (1)	2009	DBLP DOI BibTeX RDF
11	Benjamin C. Pierce	Lambda, the ultimate TA: using a proof assistant to teach programming language foundations.	ICFP	2009	DBLP DOI BibTeX RDF	programming languages, pedagogy, proof assistants
11	Nick Benton, Chung-Kil Hur	Biorthogonality, step-indexing and compiler correctness.	ICFP	2009	DBLP DOI BibTeX RDF	biorthogonality, step-indexing, denotational semantics, proof assistants, compiler verification
11	Benjamin Delaware, William R. Cook, Don S. Batory	Fitting the pieces together: a machine-checked model of safe composition.	ESEC/SIGSOFT FSE	2009	DBLP DOI BibTeX RDF	feature models, product lines, type safety
11	Benjamin Delaware, William R. Cook, Don S. Batory	A machine-checked model of safe composition.	FOAL	2009	DBLP DOI BibTeX RDF	feature model, product lines, type safety
11	Nick Benton, Nicolas Tabareau	Compiling functional types to relational specifications for low level imperative code.	TLDI	2009	DBLP DOI BibTeX RDF	separation logic, proof assistants, compiler verification, relational parametricity, type soundness
11	Amy P. Felty, Alberto Momigliano	Reasoning with hypothetical judgments and open terms in hybrid.	PPDP	2009	DBLP DOI BibTeX RDF	name-binding, induction, logical frameworks, higher-order abstract syntax, interactive theorem proving
11	Jesús Aransay, César Domínguez 0001	Modelling Differential Structures in Proof Assistants: The Graded Case.	EUROCAST	2009	DBLP DOI BibTeX RDF
11	Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie	Certified Static Analysis by Abstract Interpretation.	FOSAD	2009	DBLP DOI BibTeX RDF