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 |
|