Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
32 | Chantal Keller |
A Matter of Trust: Skeptical Communication Between Coq and External Provers. (Question de confiance : communication sceptique entre Coq et des prouveurs externes). |
|
2013 |
RDF |
|
32 | Stéphane Glondu |
Vers une certification de l'extraction de Coq. (Towards certification of the extraction of Coq). |
|
2012 |
RDF |
|
32 | Thomas Braibant |
Algèbres de Kleene, réécriture modulo AC et circuits en coq. (Kleene algebra, Rewriting modulo AC and Circuits in Coq). |
|
2012 |
RDF |
|
32 | Stéphane Lescuyer |
Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. (Formalisation et developpement d'une tactique reflexive pour la demonstration automatique en coq). |
|
2011 |
RDF |
|
32 | Bruno Barras |
Sets in Coq, Coq in Sets. |
J. Formaliz. Reason. |
2010 |
DBLP DOI BibTeX RDF |
|
32 | Elie Soubiran |
Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq. (Modular development of theories and name-space management for the Coq proof assistant). |
|
2010 |
RDF |
|
32 | Stéphane Glondu |
Extraction certifiée dans Coq-en-Coq. |
Stud. Inform. Univ. |
2009 |
DBLP BibTeX RDF |
|
32 | Stéphane Glondu |
Extraction certifiée dans Coq-en-Coq. |
JFLA |
2009 |
DBLP BibTeX RDF |
|
32 | Julien Narboux |
Formalisation et automatisation du raisonnement géométrique en Coq. (Formalisation and automation of geometric reasoning within Coq). |
|
2006 |
RDF |
|
32 | Pierre Letouzey |
Programmation fonctionnelle certifiée : L'extraction de programmes dans l'assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant). |
|
2004 |
RDF |
|
32 | Barbara Heyd |
Application de la théorie des types et du démonstrateur COQ à la vérification de programmes parallèles. (Application of type theory and the COQ assistant to the verification of parallel programs). |
|
1997 |
RDF |
|
32 | Evelyne Contejean, Andrey Paskevich, Xavier Urbain, Pierre Courtieu, Olivier Pons, Julien Forest |
A3PAT, an approach for certified automated termination proofs. |
PEPM |
2010 |
DBLP DOI BibTeX RDF |
termination, term rewriting, automated reasoning, formal proof |
32 | Adam Chlipala |
A verified compiler for an impure functional language. |
POPL |
2010 |
DBLP DOI BibTeX RDF |
compiler verification, interactive proof assistants |
32 | Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky |
Effective interactive proofs for higher-order imperative programs. |
ICFP |
2009 |
DBLP DOI BibTeX RDF |
functional programming, dependent types, separation logic, interactive proof assistants |
32 | Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal |
Ynot: dependent types for imperative programs. |
ICFP |
2008 |
DBLP DOI BibTeX RDF |
type theory, monads, Hoare logic, separation logic |
32 | Benoît Boyer, Thomas Genet, Thomas P. Jensen |
Certifying a Tree Automata Completion Checker. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
32 | Richard Bonichon, David Delahaye, Damien Doligez |
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. |
LPAR |
2007 |
DBLP DOI BibTeX RDF |
|
32 | Adam Megacz |
A coinductive monad for prop-bounded recursion. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
coinductive types, type theory |
32 | Sandrine Blazy, Zaynah Dargaye, Xavier Leroy |
Formal Verification of a C Compiler Front-End. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
32 | Nathan Whitehead |
A Certified Distributed Security Logic for Authorizing Code. |
TYPES |
2006 |
DBLP DOI BibTeX RDF |
|
32 | Virgile Prevosto, Sylvain Boulmé |
Proof Contexts with Late Binding. |
TLCA |
2005 |
DBLP DOI BibTeX RDF |
|
32 | Micaela Mayero |
Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). |
TPHOLs |
2002 |
DBLP DOI BibTeX RDF |
|
32 | Pierre Courtieu |
Proving Self-Stabilization with a Proof Assistant. |
IPDPS |
2002 |
DBLP DOI BibTeX RDF |
rewriting system on words, Self-stabilization, proof assistant |
32 | Joëlle Despeyroux |
A Higher-Order Specification of the pi-Calculus. |
IFIP TCS |
2000 |
DBLP DOI BibTeX RDF |
|
32 | Fairouz Kamareddine, François Monin |
On Automating Inductive and Non-inductive Termination Methods. |
ASIAN |
1999 |
DBLP DOI BibTeX RDF |
|
31 | Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin |
Formal certification of code-based cryptographic proofs. |
POPL |
2009 |
DBLP DOI BibTeX RDF |
cryptographic proofs, relational hoare logic, program transformations, observational equivalence, coq proof assistant |
31 | Jean-Baptiste Tristan, Xavier Leroy |
Verified validation of lazy code motion. |
PLDI |
2009 |
DBLP DOI BibTeX RDF |
lazy code motion, the coq proof assistant, redundancy elimination, translation validation, verified compilers |
31 | Xavier Leroy, Sandrine Blazy |
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. |
J. Autom. Reason. |
2008 |
DBLP DOI BibTeX RDF |
The Coq proof assistant, Compilation, C, Program verification, Memory model, Compiler correctness |
31 | Jean-Baptiste Tristan, Xavier Leroy |
Formal verification of translation validators: a case study on instruction scheduling optimizations. |
POPL |
2008 |
DBLP DOI BibTeX RDF |
the coq proof assistant, translation validation, scheduling optimizations, verified compilers |
31 | Jean-François Dufourd |
A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler's formula. |
SAC |
2007 |
DBLP DOI BibTeX RDF |
Coq system, Euler's formula, computer-aided proofs, computer-aided proofs in computational topology, genus theorem, hypermaps, formal specifications, subdivisions |
31 | Xavier Leroy |
Formal certification of a compiler back-end or: programming a compiler with a proof assistant. |
POPL |
2006 |
DBLP DOI BibTeX RDF |
compiler transformations and optimizations, the Coq theorem prover, certified compilation, program proof, semantic preservation |
31 | Mark Harman, Lin Hu 0005, Malcolm Munro, Xingyuan Zhang |
GUSTT: An Amorphous Slicing System which Combines Slicing and Transformation. |
WCRE |
2001 |
DBLP DOI BibTeX RDF |
Amorphous Slicing, Transformation, Side Effects, Coq Proof Assistant |
26 | Nick Benton, Andrew Kennedy, Carsten Varming |
Some Domain Theory and Denotational Semantics in Coq. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
26 | Max Schäfer, Torbjörn Ekman 0001, Oege de Moor |
Formalising and Verifying Reference Attribute Grammars in Coq. |
ESOP |
2009 |
DBLP DOI BibTeX RDF |
|
26 | Antonio Blanco, Enrique Freire Brañas, José Luis Freire, Javier París |
The Foldl Operator as a Coequalizer Using Coq. |
EUROCAST |
2009 |
DBLP DOI BibTeX RDF |
|
26 | Yuxin Deng, Jean-François Monin |
Verifying Self-stabilizing Population Protocols with Coq. |
TASE |
2009 |
DBLP DOI BibTeX RDF |
|
26 | Yves Bertot |
A Short Presentation of Coq. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Laurent Théry |
Proof Pearl: Revisiting the Mini-rubik in Coq. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Russell O'Connor |
Certified Exact Transcendental Real Number Computation in Coq. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Milad Niqui, Olga Tveretina |
Modular Development of Hybrid Systems for Verification in Coq. |
HSCC |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Eelis van der Weegen, James McKinna |
A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Yves Bertot |
Structural Abstract Interpretation: A Formal Study Using Coq. |
LerNet ALFA Summer School |
2008 |
DBLP DOI BibTeX RDF |
|
26 | J. Santiago Jorge, Víctor M. Gulías, Laura M. Castro |
Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
Formal methods, functional programming, software verification, real-world applications, theorem provers |
26 | Pierre Corbineau |
A Declarative Language for the Coq Proof Assistant. |
TYPES |
2007 |
DBLP DOI BibTeX RDF |
|
26 | Antonio Blanco, J. E. Freire, José Luis Freire |
Using Coq to Understand Nested Datatypes. |
EUROCAST |
2007 |
DBLP DOI BibTeX RDF |
|
26 | Pierre Lescanne |
Mechanizing common knowledge logic using COQ. |
Ann. Math. Artif. Intell. |
2006 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classifications (2000) 03B42, 03B15, 03B35 |
26 | Philippe Audebaud, Christine Paulin-Mohring |
Proofs of Randomized Algorithms in Coq. |
MPC |
2006 |
DBLP DOI BibTeX RDF |
|
26 | Ming-Hsien Tsai 0001, Bow-Yaw Wang |
Modular Formalization of Reactive Modules in COQ. |
ASIAN |
2006 |
DBLP DOI BibTeX RDF |
|
26 | Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu |
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. |
FLOPS |
2006 |
DBLP DOI BibTeX RDF |
|
26 | Benjamin Grégoire, Assia Mahboubi |
Proving Equalities in a Commutative Ring Done Right in Coq. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
26 | Julien Narboux |
A Decision Procedure for Geometry in Coq. |
TPHOLs |
2004 |
DBLP DOI BibTeX RDF |
|
26 | June Andronick, Boutheina Chetali, Olivier Ly |
Using Coq to Verify Java Card Applet Isolation Properties. |
TPHOLs |
2003 |
DBLP DOI BibTeX RDF |
Security, Theorem Proving, Smart Card |
26 | David Cachera, David Pichardie |
Embedding of Systems of Affine Recurrence Equations in Coq. |
TPHOLs |
2003 |
DBLP DOI BibTeX RDF |
|
26 | Furio Honsell, Ivan Scagnetto |
Mobility Types in Coq. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
26 | José Luis Freire-Nistal, Antonio Blanco Ferro, Víctor M. Gulías, José E. Freire Brañas |
On the Strong Co-induction in Coq. |
EUROCAST |
2003 |
DBLP DOI BibTeX RDF |
|
26 | Gilles Barthe, Pierre Courtieu |
Efficient Reasoning about Executable Specifications in Coq. |
TPHOLs |
2002 |
DBLP DOI BibTeX RDF |
|
26 | Xavier Rival, Jean Goubault-Larrecq |
Experiments with Finite Tree Automata in Coq. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
26 | Catherine Dubois |
Proving ML Type Soundness Within Coq. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
26 | Vincent Zammit |
A Comparative Study of Coq and HOL. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
26 | Christine Paulin-Mohring |
Circuits as Streams in Coq: Verification of a Sequential Multiplier. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
26 | Joëlle Despeyroux, André Hirschowitz |
Higher-Order Abstract Syntax with Induction in Coq. |
LPAR |
1994 |
DBLP DOI BibTeX RDF |
|
21 | Zachary Tatlock, Sorin Lerner |
Bringing extensibility to verified compilers. |
PLDI |
2010 |
DBLP DOI BibTeX RDF |
compiler optimization, correctness, extensibility |
21 | Ulf Norell |
Dependently typed programming in Agda. |
TLDI |
2009 |
DBLP DOI BibTeX RDF |
programming, dependent types |
21 | Adam Chlipala |
Parametric higher-order abstract syntax for mechanized semantics. |
ICFP |
2008 |
DBLP DOI BibTeX RDF |
type-theoretic semantics, dependent types, compiler verification, interactive proof assistants |
21 | Nicolas Oury |
Pattern matching coverage checking with dependent types using set approximations. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
coverage checking, set approximation, pattern matching |
21 | Sylvie Boldo, Jean-Christophe Filliâtre |
Formal Verification of Floating-Point Programs. |
IEEE Symposium on Computer Arithmetic |
2007 |
DBLP DOI BibTeX RDF |
|
21 | Ralph Matthes, Martin Strecker |
Verification of the Redecoration Algorithm for Triangular Matrices. |
TYPES |
2007 |
DBLP DOI BibTeX RDF |
|
21 | José Luis Freire-Nistal, Enrique Freire Brañas, Antonio Blanco Ferro, David Cabrero Souto |
On the Representation of Imperative Programs in a Logical Framework. |
EUROCAST |
2007 |
DBLP DOI BibTeX RDF |
|
21 | Georges Gonthier |
The Four Colour Theorem: Engineering of a Formal Proof. |
ASCM |
2007 |
DBLP DOI BibTeX RDF |
|
21 | Milad Niqui |
Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers. |
TYPES |
2006 |
DBLP DOI BibTeX RDF |
|
21 | Adam Chlipala |
Modular development of certified program verifiers with a proof assistant. |
ICFP |
2006 |
DBLP DOI BibTeX RDF |
programming with dependent types, proof-carrying code, interactive proof assistants |
21 | Adam Koprowski |
Certified Higher-Order Recursive Path Ordering. |
RTA |
2006 |
DBLP DOI BibTeX RDF |
|
21 | Sandrine Blazy, Xavier Leroy |
Formal Verification of a Memory Model for C-Like Imperative Languages. |
ICFEM |
2005 |
DBLP DOI BibTeX RDF |
|
21 | Bruno Barras, Benjamin Grégoire |
On the Role of Type Decorations in the Calculus of Inductive Constructions. |
CSL |
2005 |
DBLP DOI BibTeX RDF |
|
21 | David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu |
Extracting a Data Flow Analyser in Constructive Logic. |
ESOP |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Jean-Christophe Filliâtre, Pierre Letouzey |
Functors for Proofs and Programs. |
ESOP |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Dachuan Yu, Zhong Shao |
Verification of safety properties for concurrent assembly code. |
ICFP |
2004 |
DBLP DOI BibTeX RDF |
local guarantee, concurrency, assembly |
21 | Evelyne Contejean |
A Certified AC Matching Algorithm. |
RTA |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Etsuya Shibayama, Shigeki Hagihara, Naoki Kobayashi 0001, Shin-ya Nishizaki, Kenjiro Taura, Takuo Watanabe |
AnZenMail: A Secure and Certified E-mail System. |
ISSS |
2002 |
DBLP DOI BibTeX RDF |
|
21 | David Delahaye |
Free-Style Theorem Proving. |
TPHOLs |
2002 |
DBLP DOI BibTeX RDF |
|
21 | Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu 0005 |
Mechanized Operational Semantics of WSL. |
SCAM |
2002 |
DBLP DOI BibTeX RDF |
Computer Assisted Formal Reasoning, Program Transformation |
21 | Sylvain Boulmé, Grégoire Hamon |
Certifying Synchrony for Free. |
LPAR |
2001 |
DBLP DOI BibTeX RDF |
|
21 | Ewen Denney |
The Synthesis of a Java Card Tokenization Algorithm. |
ASE |
2001 |
DBLP DOI BibTeX RDF |
|
21 | Hui Jiang 0004, Dong Lin, Xiren Xie |
Embedding UML and Type Theory to Formalize the Process of Requirement Engineering. |
TOOLS (36) |
2000 |
DBLP DOI BibTeX RDF |
|
21 | Yves Bertot |
The CtCoq System: Design and Architecture. |
Formal Aspects Comput. |
1999 |
DBLP DOI BibTeX RDF |
Interactive proof development, CtCoq, Proof by pointing, Proof maintenance, Graphical user interfaces |
21 | Laurent Théry |
A Certified Version of Buchberger's Algorithm. |
CADE |
1998 |
DBLP DOI BibTeX RDF |
|
21 | Furio Honsell, Marino Miculan |
A Natural Deduction Approach to Dynamic Logic. |
TYPES |
1995 |
DBLP DOI BibTeX RDF |
|
21 | Gérard P. Huet |
The Gallina Specification language: A Case Study. |
FSTTCS |
1992 |
DBLP DOI BibTeX RDF |
|
21 | Nassima Izerrouken, Marc Pantel, Xavier Thirioux |
Machine-Checked Sequencer for Critical Embedded Code Generator. |
ICFEM |
2009 |
DBLP DOI BibTeX RDF |
block sequencing, software engineering, formal verification, automatic code generator, Coq proof assistant |
21 | Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai |
Integrated Formal Approach for Qualified Critical Embedded Code Generator. |
FMICS |
2009 |
DBLP DOI BibTeX RDF |
formal verification, automatic code generator, qualification, Coq proof assistant |
16 | Joshua M. Cohen, Philip Johnson-Freyd |
A Formalization of Core Why3 in Coq. |
Proc. ACM Program. Lang. |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Wenjun Shi, Qinxiang Cao, Yuxin Deng |
Formalizing the Semantics of a Classical-Quantum Imperative Language in Coq. |
J. Circuits Syst. Comput. |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Noé De Santo, Aurèle Barrière, Clément Pit-Claudel |
A Coq Mechanization of JavaScript Regular Expression Semantics. |
CoRR |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Reynald Affeldt, Zachary Stone |
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. |
CoRR |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark |
Taming Differentiable Logics with Coq Formalisation. |
CoRR |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Andreas Florath |
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code. |
CoRR |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Mallku Soldevila, Rodrigo Ribeiro, Beta Ziliani |
Redex -> Coq: towards a theory of decidability of Redex's reduction semantics. |
CoRR |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Nicolas Magaud |
Towards Automatic Transformations of Coq Proof Scripts. |
CoRR |
2024 |
DBLP DOI BibTeX RDF |
|
16 | David Braun, Nicolas Magaud, Pascal Schreck |
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry. |
J. Autom. Reason. |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Wenxuan Tao, Gang Chen |
A Coq-Based Infrastructure for Quantum Programming, Verification and Simulation. |
TAMC |
2024 |
DBLP DOI BibTeX RDF |
|