Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
16 | Jónathan Heras, Ekaterina Komendantskaya |
ML4PG: proof-mining in Coq |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Jan Olaf Blech, Sidi Ould Biha |
On Formal Reasoning on the Semantics of PLC using Coq |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
Implementing and reasoning about hash-consed data structures in Coq. |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine |
Homotopy limits in Coq |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous |
Formal verification in Coq of program properties involving the global state effect. |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Lionel Rieg |
Extracting Herbrand trees from Coq |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Jónathan Heras, Ekaterina Komendantskaya |
Statistical Proof-Patterns in Coq/SSReflect |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Damien Pous |
Kleene Algebra with Tests and Coq Tools for While Programs |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
Implementing hash-consed structures in Coq |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Makarius Wenzel |
PIDE as front-end technology for Coq |
CoRR |
2013 |
DBLP BibTeX RDF |
|
16 | Adam Chlipala |
Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. |
|
2013 |
RDF |
|
16 | Dongxi Liu, Neale Leslie Fulton, John Zic, Martin de Groot |
Verifying an Aircraft Proximity Characterization Method in Coq. |
ICFEM |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis |
Mtac: a monad for typed tactic programming in Coq. |
ICFP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Pierre Courtieu, Maria-Virginia Aponte, Tristan Crolard, Zhi Zhang, Robby, Jason Belt, John Hatcliff, Jérôme Guitton, Trevor Jennings |
Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. |
HILT |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Nada Habli, Amy P. Felty |
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Richard Dapoigny, Patrick Barlatier |
Modeling Ontological Structures with Type Classes in Coq. |
ICCS |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Hendrik Tews |
Formalizing Cut Elimination of Coalgebraic Logics in Coq. |
TABLEAUX |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Jael Kriener, Andy King, Sandrine Blazy |
Proofs you can believe in: proving equivalences between Prolog semantics in Coq. |
PPDP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Wojciech Jedynak, Malgorzata Biernacka, Dariusz Biernacki |
An operational foundation for the tactic language of Coq. |
PPDP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Andrew Kennedy, Nick Benton, Jonas Braband Jensen, Pierre-Évariste Dagand |
Coq: the world's best macro assembler? |
PPDP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Yi Li 0010, Meng Sun 0002 |
Modeling and Analysis of Component Connectors in Coq. |
FACS |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Frédéric Loulergue, Virginia Niculescu, Simon Robillard |
Powerlists in Coq: Programming and Reasoning. |
CANDAR |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Cyril Cohen |
Pragmatic Quotient Types in Coq. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Jörg Endrullis, Dimitri Hendriks, Martin Bodin |
Circular Coinduction in Coq Using Bisimulation-Up-To Techniques. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Assia Mahboubi, Enrico Tassi |
Canonical Structures for the Working Coq User. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
Implementing Hash-Consed Structures in Coq. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Evgeny Makarov, Bas Spitters |
The Picard Algorithm for Ordinary Differential Equations in Coq. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Damien Pous |
Kleene Algebra with Tests and Coq Tools for while Programs. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Robbert Krebbers |
Aliasing Restrictions of C11 Formalized in Coq. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka |
A Constructive Theory of Regular Languages in Coq. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Gordon Stewart 0001 |
Computational Verification of Network Programs in Coq. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela Mayero, Ioana Pasca |
Certified, Efficient and Sharp Univariate Taylor Models in COQ. |
SYNASC |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Ken Madlener, Sjaak Smetsers |
GSOS Formalized in Coq. |
TASE |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Nicolas Magaud, Julien Narboux, Pascal Schreck |
A case study in formalizing projective geometry in Coq: Desargues theorem. |
Comput. Geom. |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Christophe Brun, Jean-François Dufourd, Nicolas Magaud |
Designing and proving correct a convex hull algorithm with hypermaps in Coq. |
Comput. Geom. |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Damien Pous |
Deciding Kleene Algebras in Coq |
Log. Methods Comput. Sci. |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles |
Computing Persistent Homology within Coq/SSReflect |
CoRR |
2012 |
DBLP BibTeX RDF |
|
16 | Frédéric Blanqui, Adam Koprowski |
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. |
CoRR |
2012 |
DBLP BibTeX RDF |
|
16 | Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride |
Strongly Typed Term Representations in Coq. |
J. Autom. Reason. |
2012 |
DBLP DOI BibTeX RDF |
|
16 | André Hirschowitz, Marco Maggesi |
Nested Abstract Syntax in Coq. |
J. Autom. Reason. |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Guillaume Melquiond |
Floating-point arithmetic in the Coq system. |
Inf. Comput. |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Christophe Brun, Jean-François Dufourd, Nicolas Magaud |
Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls. |
Automated Deduction in Geometry |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Nelma Moreira, David Pereira, Simão Melo de Sousa |
Deciding Regular Expressions (In-)Equivalence in Coq. |
RAMiCS |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen 0002 |
Self-certification: bootstrapping certified typecheckers in F* with Coq. |
POPL |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Vladimir Komendantsky |
Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect. |
PLPV |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, Nicholas Cameron 0001 |
Encoding Featherweight Java with assignment and immutability using the Coq proof assistant. |
FTfJP@ECOOP |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Dimitur Nikolaev Krustev |
Towards a Framework for Building Formally Verified Supercompilers in Coq. |
Trends in Functional Programming |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Reynald Affeldt, Manabu Hagiwara |
Formalization of Shannon's Theorems in SSReflect-Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Cyril Cohen |
Construction of Real Algebraic Numbers in Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal |
Charge! - A Framework for Higher-Order Separation Logic in Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Marino Miculan, Marco Paviotti |
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Maxime Dénès, Anders Mörtberg, Vincent Siles |
A Refinement-Based Approach to Computational Algebra in Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Raymond McCarthy Bergeron |
La lune et le coq. |
SIGGRAPH Computer Animation Festival |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Sylvie Boldo, Catherine Lelay, Guillaume Melquiond |
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Nicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry |
Rigorous Polynomial Approximation Using Taylor Models in Coq. |
NASA Formal Methods |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Wouter Swierstra |
xmonad in Coq (experience report): programming a window manager in a proof assistant. |
Haskell |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Jesse Alama, Lionel Mamane, Josef Urban |
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar. |
AISC/MKM/Calculemus |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Hai Wan, Gang Chen 0004, Xiaoyu Song, Ming Gu 0001 |
Formalisation and verification of programmable logic controllers timers in Coq. |
IET Softw. |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Frédéric Blanqui, Adam Koprowski |
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. |
Math. Struct. Comput. Sci. |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai |
Expérimentations en Coq pour un générateur de code qualifiable. |
Tech. Sci. Informatiques |
2011 |
DBLP DOI BibTeX RDF |
|
16 | César Domínguez 0001, Julio Rubio 0001 |
Effective homology of bicomplexes, formalized in Coq. |
Theor. Comput. Sci. |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Benedikt Ahrens, Julianna Zsido |
Initial Semantics for higher-order typed syntax in Coq. |
J. Formaliz. Reason. |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Damien Pous |
Tactics for Reasoning modulo AC in Coq |
CoRR |
2011 |
DBLP BibTeX RDF |
|
16 | Thomas Braibant |
Coquet: a Coq library for verifying hardware |
CoRR |
2011 |
DBLP BibTeX RDF |
|
16 | Robbert Krebbers, Bas Spitters |
Type classes for efficient exact real arithmetic in Coq |
Log. Methods Comput. Sci. |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jan Olaf Blech |
A Tool for the Certification of PLCs based on a Coq Semantics for Sequential Function Charts |
CoRR |
2011 |
DBLP BibTeX RDF |
|
16 | Robbert Krebbers, Bas Spitters |
Computer certified efficient exact reals in Coq |
CoRR |
2011 |
DBLP BibTeX RDF |
|
16 | Emmanuel Polonowski |
Generic Environments in Coq |
CoRR |
2011 |
DBLP BibTeX RDF |
|
16 | Stéphane Lescuyer |
First-Class Containers in Coq. |
Stud. Inform. Univ. |
2011 |
DBLP BibTeX RDF |
|
16 | Christine Paulin-Mohring |
Introduction to the Coq Proof-Assistant for Practical Software Verification. |
LASER Summer School |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Sylvie Boldo, Guillaume Melquiond |
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. |
IEEE Symposium on Computer Arithmetic |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Aloïs Brunel |
Non-constructive complex analysis in Coq. |
TYPES |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Sidi Ould Biha |
A Formal Semantics of PLC Programs in Coq. |
COMPSAC |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal |
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza |
Structural Analysis of Narratives with the Coq Proof Assistant. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Tuan-Minh Pham, Yves Bertot, Julien Narboux |
A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. |
ICCSA (4) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Martin Henz, Aquinas Hobor |
Teaching Experience: Logic and Formal Methods with Coq. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant |
Coquet: A Coq Library for Verifying Hardware. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Damien Pous |
Tactics for Reasoning Modulo AC in Coq. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner |
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie |
Modular SMT Proofs for Fast Reflexive Checking Inside Coq. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jieung Kim, Sukyoung Ryu |
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jean-David Génevaux, Julien Narboux, Pascal Schreck |
Formalization of Wu's Simple Method in Coq. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jan Olaf Blech, Sidi Ould Biha |
Verification of PLC Properties Based on Formal Semantics in Coq. |
SEFM |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, Masami Hagiya |
Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications. |
SEFM |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Robbert Krebbers, Bas Spitters |
Computer Certified Efficient Exact Reals in Coq. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Vladimir Komendantsky, Alexander Konovalov 0001, Steve Linton |
View of Computer Algebra Data from Coq. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau |
Incidence Simplicial Matrices Formalized in Coq/SSReflect. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Robbert Krebbers, Freek Wiedijk |
A Formalization of the C99 Standard in HOL, Isabelle and Coq. |
Calculemus/MKM |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Hermann Lehner |
A formal definition of JML in Coq and its application to runtime assertion checking. |
|
2011 |
RDF |
|
16 | Vladimir Komendantsky, Alexander Konovalov 0001, Steve Linton |
Interfacing Coq + SSReflect with GAP. |
UITP |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Gang Chen |
Formalization of a Parameterized Parallel Adder Within the Coq Theorem Prover. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Georges Gonthier, Assia Mahboubi |
An introduction to small scale reflection in Coq. |
J. Formaliz. Reason. |
2010 |
DBLP DOI BibTeX RDF |
|
16 | José Grimm |
Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. |
J. Formaliz. Reason. |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Adam Chlipala |
An Introduction to Programming and Proving with Dependent Types in Coq. |
J. Formaliz. Reason. |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Loïc Pottier |
Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics |
CoRR |
2010 |
DBLP BibTeX RDF |
|
16 | César Domínguez 0001, Julio Rubio 0001 |
Computing in Coq with Infinite Algebraic Data Structures |
CoRR |
2010 |
DBLP BibTeX RDF |
|
16 | Christine Choppy, Micaela Mayero, Laure Petrucci |
Coloured Petri net refinement specification and correctness proof with Coq. |
Innov. Syst. Softw. Eng. |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Laurent Fuchs, Laurent Théry |
A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry. |
Automated Deduction in Geometry |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Filip Sieczkowski, Malgorzata Biernacka, Dariusz Biernacki |
Automating Derivations of Abstract Machines from Reduction Semantics: - A Generic Formalization of Refocusing in Coq. |
IFL |
2010 |
DBLP DOI BibTeX RDF |
|