Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
16 | Jónathan Heras, Ekaterina Komendantskaya |
ML4PG: proof-mining in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1302.6421, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Jan Olaf Blech, Sidi Ould Biha |
On Formal Reasoning on the Semantics of PLC using Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1301.3047, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
Implementing and reasoning about hash-consed data structures in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1311.2959, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine |
Homotopy limits in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1304.0680, 2013. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1310.0794, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Lionel Rieg |
Extracting Herbrand trees from Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1304.4557, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Jónathan Heras, Ekaterina Komendantskaya |
Statistical Proof-Patterns in Coq/SSReflect ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1301.6039, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Damien Pous |
Kleene Algebra with Tests and Coq Tools for While Programs ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1302.1737, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
Implementing hash-consed structures in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1304.6038, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Makarius Wenzel |
PIDE as front-end technology for Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1304.6626, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
16 | Adam Chlipala |
Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2013 |
RDF |
|
16 | Dongxi Liu, Neale Leslie Fulton, John Zic, Martin de Groot |
Verifying an Aircraft Proximity Characterization Method in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, October 29 - November 1, 2013, Proceedings, pp. 86-101, 2013, Springer, 978-3-642-41201-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pp. 87-100, 2013, ACM, 978-1-4503-2326-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HILT ![In: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, HILT 2013, Pittsburgh, Pennsylvania, USA, November 10-14, 2013, pp. 21-22, 2013, ACM, 978-1-4503-2467-0. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Nada Habli, Amy P. Felty |
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP@CADE ![In: Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013, pp. 67-76, 2013, EasyChair. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Richard Dapoigny, Patrick Barlatier |
Modeling Ontological Structures with Type Classes in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCS ![In: Conceptual Structures for STEM Research and Education, 20th International Conference on Conceptual Structures, ICCS 2013, Mumbai, India, January 10-12, 2013. Proceedings, pp. 135-152, 2013, Springer, 978-3-642-35785-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Hendrik Tews |
Formalizing Cut Elimination of Coalgebraic Logics in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013. Proceedings, pp. 257-272, 2013, Springer, 978-3-642-40536-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Jael Kriener, Andy King, Sandrine Blazy |
Proofs you can believe in: proving equivalences between Prolog semantics in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Madrid, Spain, September 16-18, 2013, pp. 37-48, 2013, ACM, 978-1-4503-2154-9. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Wojciech Jedynak, Malgorzata Biernacka, Dariusz Biernacki |
An operational foundation for the tactic language of Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Madrid, Spain, September 16-18, 2013, pp. 25-36, 2013, ACM, 978-1-4503-2154-9. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Andrew Kennedy, Nick Benton, Jonas Braband Jensen, Pierre-Évariste Dagand |
Coq: the world's best macro assembler? ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Madrid, Spain, September 16-18, 2013, pp. 13-24, 2013, ACM, 978-1-4503-2154-9. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Yi Li 0010, Meng Sun 0002 |
Modeling and Analysis of Component Connectors in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FACS ![In: Formal Aspects of Component Software - 10th International Symposium, FACS 2013, Nanchang, China, October 27-29, 2013, Revised Selected Papers, pp. 273-290, 2013, Springer, 978-3-319-07601-0. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Frédéric Loulergue, Virginia Niculescu, Simon Robillard |
Powerlists in Coq: Programming and Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CANDAR ![In: The First International Symposium on Computing and Networking - Across Practical Development and Theoretical Research, Dogo SPA Resort, Matsuyama, Japan, December 4-6, 2013., pp. 57-65, 2013, IEEE Computer Society, 978-1-4799-2795-1. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Cyril Cohen |
Pragmatic Quotient Types in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 213-228, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Jörg Endrullis, Dimitri Hendriks, Martin Bodin |
Circular Coinduction in Coq Using Bisimulation-Up-To Techniques. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 354-369, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Assia Mahboubi, Enrico Tassi |
Canonical Structures for the Working Coq User. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 19-34, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
Implementing Hash-Consed Structures in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 477-483, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Evgeny Makarov, Bas Spitters |
The Picard Algorithm for Ordinary Differential Equations in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 463-468, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Damien Pous |
Kleene Algebra with Tests and Coq Tools for while Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 180-196, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Robbert Krebbers |
Aliasing Restrictions of C11 Formalized in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, pp. 50-65, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka |
A Constructive Theory of Regular Languages in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, pp. 82-97, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Gordon Stewart 0001 |
Computational Verification of Network Programs in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, pp. 33-49, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SYNASC ![In: 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, September 23-26, 2013, pp. 193-200, 2013, IEEE Computer Society, 978-1-4799-3035-7. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Ken Madlener, Sjaak Smetsers |
GSOS Formalized in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, 1-3 July 2013, Birmingham, UK, pp. 199-206, 2013, IEEE Computer Society, 978-0-7695-5053-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Nicolas Magaud, Julien Narboux, Pascal Schreck |
A case study in formalizing projective geometry in Coq: Desargues theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Geom. ![In: Comput. Geom. 45(8), pp. 406-424, 2012. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Geom. ![In: Comput. Geom. 45(8), pp. 436-457, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Damien Pous |
Deciding Kleene Algebras in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. Methods Comput. Sci. ![In: Log. Methods Comput. Sci. 8(1), 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles |
Computing Persistent Homology within Coq/SSReflect ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1209.1905, 2012. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1202.6473, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP BibTeX RDF |
|
16 | Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride |
Strongly Typed Term Representations in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 49(2), pp. 141-159, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | André Hirschowitz, Marco Maggesi |
Nested Abstract Syntax in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 49(3), pp. 409-426, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Guillaume Melquiond |
Floating-point arithmetic in the Coq system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Comput. ![In: Inf. Comput. 216, pp. 14-23, 2012. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry - 9th International Workshop, ADG 2012, Edinburgh, UK, September 17-19, 2012. Revised Selected Papers, pp. 71-88, 2012, Springer, 978-3-642-40671-3. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Nelma Moreira, David Pereira, Simão Melo de Sousa |
Deciding Regular Expressions (In-)Equivalence in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RAMiCS ![In: Relational and Algebraic Methods in Computer Science - 13th International Conference, RAMiCS 2012, Cambridge, UK, September 17-20, 2012. Proceedings, pp. 98-113, 2012, Springer, 978-3-642-33313-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pp. 571-584, 2012, ACM, 978-1-4503-1083-3. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Vladimir Komendantsky |
Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012, pp. 61-70, 2012, ACM, 978-1-4503-1125-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FTfJP@ECOOP ![In: Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP 2012, Beijing, China, June 12, 2012, pp. 11-19, 2012, ACM, 978-1-4503-1272-1. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Dimitur Nikolaev Krustev |
Towards a Framework for Building Formally Verified Supercompilers in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Trends in Functional Programming ![In: Trends in Functional Programming - 13th International Symposium, TFP 2012, St. Andrews, UK, June 12-14, 2012, Revised Selected Papers, pp. 133-148, 2012, Springer, 978-3-642-40446-7. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Reynald Affeldt, Manabu Hagiwara |
Formalization of Shannon's Theorems in SSReflect-Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pp. 233-249, 2012, Springer, 978-3-642-32346-1. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Cyril Cohen |
Construction of Real Algebraic Numbers in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pp. 67-82, 2012, Springer, 978-3-642-32346-1. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal |
Charge! - A Framework for Higher-Order Separation Logic in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pp. 315-331, 2012, Springer, 978-3-642-32346-1. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Marino Miculan, Marco Paviotti |
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pp. 183-200, 2012, Springer, 978-3-642-32346-1. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Maxime Dénès, Anders Mörtberg, Vincent Siles |
A Refinement-Based Approach to Computational Algebra in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pp. 83-98, 2012, Springer, 978-3-642-32346-1. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Raymond McCarthy Bergeron |
La lune et le coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIGGRAPH Computer Animation Festival ![In: International Conference on Computer Graphics and Interactive Techniques, SIGGRAPH 2012, Los Angeles, California, USA, August 5-9, 2012, Computer Animation Festival, pp. 44, 2012, ACM, 978-1-4503-1677-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings, pp. 289-304, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NASA Formal Methods ![In: NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, pp. 85-99, 2012, Springer, 978-3-642-28890-6. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Wouter Swierstra |
xmonad in Coq (experience report): programming a window manager in a proof assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Haskell ![In: Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Haskell 2012, Copenhagen, Denmark, 13 September 2012, pp. 131-136, 2012, ACM, 978-1-4503-1574-6. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
16 | Jesse Alama, Lionel Mamane, Josef Urban |
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC/MKM/Calculemus ![In: Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings, pp. 1-16, 2012, Springer, 978-3-642-31373-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IET Softw. ![In: IET Softw. 5(1), pp. 32-42, 2011. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Math. Struct. Comput. Sci. ![In: Math. Struct. Comput. Sci. 21(4), pp. 827-859, 2011. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Tech. Sci. Informatiques ![In: Tech. Sci. Informatiques 30(4), pp. 409-440, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | César Domínguez 0001, Julio Rubio 0001 |
Effective homology of bicomplexes, formalized in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 412(11), pp. 962-970, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Benedikt Ahrens, Julianna Zsido |
Initial Semantics for higher-order typed syntax in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Formaliz. Reason. ![In: J. Formaliz. Reason. 4(1), pp. 25-69, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Damien Pous |
Tactics for Reasoning modulo AC in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1106.4448, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
16 | Thomas Braibant |
Coquet: a Coq library for verifying hardware ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1108.4253, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
16 | Robbert Krebbers, Bas Spitters |
Type classes for efficient exact real arithmetic in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. Methods Comput. Sci. ![In: Log. Methods Comput. Sci. 9(1), 2011. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1102.3529, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
16 | Robbert Krebbers, Bas Spitters |
Computer certified efficient exact reals in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1105.2751, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
16 | Emmanuel Polonowski |
Generic Environments in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1112.1316, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
16 | Stéphane Lescuyer |
First-Class Containers in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Stud. Inform. Univ. ![In: Stud. Inform. Univ. 9(1), pp. 87-127, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
16 | Christine Paulin-Mohring |
Introduction to the Coq Proof-Assistant for Practical Software Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LASER Summer School ![In: Tools for Practical Software Verification, LASER, International Summer School 2011, Elba Island, Italy, Revised Tutorial Lectures, pp. 45-95, 2011, Springer, 978-3-642-35745-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Sylvie Boldo, Guillaume Melquiond |
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Symposium on Computer Arithmetic ![In: 20th IEEE Symposium on Computer Arithmetic, ARITH 2011, Tübingen, Germany, 25-27 July 2011, pp. 243-252, 2011, IEEE Computer Society, 978-0-7695-4318-5. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Aloïs Brunel |
Non-constructive complex analysis in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 18th International Workshop on Types for Proofs and Programs, TYPES 2011, September 8-11, 2011, Bergen, Norway, pp. 1-15, 2011, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-939897-49-1. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Sidi Ould Biha |
A Formal Semantics of PLC Programs in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COMPSAC ![In: Proceedings of the 35th Annual IEEE International Computer Software and Applications Conference, COMPSAC 2011, Munich, Germany, 18-22 July 2011, pp. 118-127, 2011, IEEE Computer Society, 978-0-7695-4439-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, pp. 22-38, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza |
Structural Analysis of Narratives with the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, pp. 55-70, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCSA (4) ![In: Computational Science and Its Applications - ICCSA 2011 - International Conference, Santander, Spain, June 20-23, 2011. Proceedings, Part IV, pp. 368-383, 2011, Springer, 978-3-642-21897-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Martin Henz, Aquinas Hobor |
Teaching Experience: Logic and Formal Methods with Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, pp. 199-215, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant |
Coquet: A Coq Library for Verifying Hardware. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, pp. 330-345, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Damien Pous |
Tactics for Reasoning Modulo AC in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, pp. 167-182, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, pp. 135-150, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie |
Modular SMT Proofs for Fast Reflexive Checking Inside Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, pp. 151-166, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jieung Kim, Sukyoung Ryu |
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, pp. 264-279, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jean-David Génevaux, Julien Narboux, Pascal Schreck |
Formalization of Wu's Simple Method in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, pp. 71-86, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Jan Olaf Blech, Sidi Ould Biha |
Verification of PLC Properties Based on Formal Semantics in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings, pp. 58-73, 2011, Springer, 978-3-642-24689-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings, pp. 350-365, 2011, Springer, 978-3-642-24689-0. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Robbert Krebbers, Bas Spitters |
Computer Certified Efficient Exact Reals in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings, pp. 90-106, 2011, Springer, 978-3-642-22672-4. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Vladimir Komendantsky, Alexander Konovalov 0001, Steve Linton |
View of Computer Algebra Data from Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings, pp. 74-89, 2011, Springer, 978-3-642-22672-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings, pp. 30-44, 2011, Springer, 978-3-642-22672-4. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Robbert Krebbers, Freek Wiedijk |
A Formalization of the C99 Standard in HOL, Isabelle and Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings, pp. 301-303, 2011, Springer, 978-3-642-22672-4. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
16 | Hermann Lehner |
A formal definition of JML in Coq and its application to runtime assertion checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2011 |
RDF |
|
16 | Vladimir Komendantsky, Alexander Konovalov 0001, Steve Linton |
Interfacing Coq + SSReflect with GAP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
UITP ![In: Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, UITP 2010, Edinburgh, UK, July 15, 2010, pp. 17-28, 2010, Elsevier. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Gang Chen |
Formalization of a Parameterized Parallel Adder Within the Coq Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. ![In: IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(1), pp. 149-153, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Georges Gonthier, Assia Mahboubi |
An introduction to small scale reflection in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Formaliz. Reason. ![In: J. Formaliz. Reason. 3(2), pp. 95-152, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | José Grimm |
Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Formaliz. Reason. ![In: J. Formaliz. Reason. 3(1), pp. 79-126, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Adam Chlipala |
An Introduction to Programming and Proving with Dependent Types in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Formaliz. Reason. ![In: J. Formaliz. Reason. 3(2), pp. 1-93, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Loïc Pottier |
Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1007.3615, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP BibTeX RDF |
|
16 | César Domínguez 0001, Julio Rubio 0001 |
Computing in Coq with Infinite Algebraic Data Structures ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1004.4998, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP BibTeX RDF |
|
16 | Christine Choppy, Micaela Mayero, Laure Petrucci |
Coloured Petri net refinement specification and correctness proof with Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Innov. Syst. Softw. Eng. ![In: Innov. Syst. Softw. Eng. 6(3), pp. 195-202, 2010. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry - 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers, pp. 51-67, 2010, Springer, 978-3-642-25069-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFL ![In: Implementation and Application of Functional Languages - 22nd International Symposium, IFL 2010, Alphen aan den Rijn, The Netherlands, September 1-3, 2010, Revised Selected Papers, pp. 72-88, 2010, Springer, 978-3-642-24275-5. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|