Search results for "Coq"

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