Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
16 | Iman Poernomo, Jeffrey Terrell |
Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings, pp. 56-73, 2010, Springer, 978-3-642-16900-7. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi |
Program Calculation in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology - 13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010. Revised Selected Papers, pp. 163-179, 2010, Springer, 978-3-642-17795-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | José Bacelar Almeida, Nelma Moreira, David Pereira, Simão Melo de Sousa |
Partial Derivative Automata Formalized in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CIAA ![In: Implementation and Application of Automata - 15th International Conference, CIAA 2010, Winnipeg, MB, Canada, August 12-15, 2010. Revised Selected Papers, pp. 59-68, 2010, Springer, 978-3-642-18097-2. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Adam Chlipala |
Foundational Program Verification in Coq with Automated Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MSFP@ICFP ![In: Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010., pp. 19, 2010, ACM, 978-1-4503-0255-5. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Amy P. Felty |
Hybrid: Reasoning with Higher-Order Abstract Syntax in Coq and Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MSFP@ICFP ![In: Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010., pp. 1-2, 2010, ACM, 978-1-4503-0255-5. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Martin Hofmann 0001, Aleksandr Karbyshev, Helmut Seidl |
Verifying a Local Generic Solver in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAS ![In: Static Analysis - 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010. Proceedings, pp. 340-355, 2010, Springer, 978-3-642-15768-4. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Chantal Keller, Benjamin Werner |
Importing HOL Light into Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 307-322, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Bas Spitters, Eelis van der Weegen |
Developing the Algebraic Hierarchy with Type Classes in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 490-493, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 83-98, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Damien Pous |
An Efficient Coq Tactic for Deciding Kleene Algebras. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 163-178, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Pierre-Yves Strub |
Coq Modulo Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, pp. 529-543, 2010, Springer, 978-3-642-15204-7. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Maciej Piróg, Dariusz Biernacki |
A systematic derivation of the STG machine verified in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Haskell ![In: Proceedings of the 3rd ACM SIGPLAN Symposium on Haskell, Haskell 2010, Baltimore, MD, USA, 30 September 2010, pp. 25-36, 2010, ACM, 978-1-4503-0252-4. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI 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) |
AISC/MKM/Calculemus ![In: Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings, pp. 204-218, 2010, Springer, 978-3-642-14127-0. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Hai Wan, Xiaoyu Song, Ming Gu 0001 |
Parameterized Specification and Verification of PLC Systems in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2010, Taipei, Taiwan, 25-27 August 2010, pp. 179-182, 2010, IEEE Computer Society, 978-0-7695-4148-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
16 | Adam Koprowski |
Coq formalization of the higher-order recursive path ordering. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Algebra Eng. Commun. Comput. ![In: Appl. Algebra Eng. Commun. Comput. 20(5-6), pp. 379-425, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
16 | Philippe Audebaud, Christine Paulin-Mohring |
Proofs of randomized algorithms in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sci. Comput. Program. ![In: Sci. Comput. Program. 74(8), pp. 568-589, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
16 | Wendy Verbruggen, Edsko de Vries, Arthur Hughes |
Polytypic properties and proofs in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WGP@ICFP ![In: Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming, WGP@ICFP 2009, Edinburgh, United Kingdom, August 31 - September 2, 2009, pp. 1-12, 2009, ACM, 978-1-60558-510-9. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
16 | Daniel W. H. James, Ralf Hinze |
A Reflection-based Proof Tactic for Lattices in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Trends in Functional Programming ![In: Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009, Komárno, Slovakia, June 2-4, 2009., pp. 97-112, 2009, Intellect, 978-1-84150-405-6. The full citation details ...](Pics/full.jpeg) |
2009 |
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) |
NASA Formal Methods ![In: First NASA Formal Methods Symposium - NFM 2009, Moffett Field, California, USA, April 6-8, 2009., pp. 156-165, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP BibTeX RDF |
|
16 | Yves Bertot, Ekaterina Komendantskaya |
Inductive and Coinductive Components of Corecursive Functions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CMCS ![In: Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008, Budapest, Hungary, April 4-6, 2008, pp. 25-47, 2008, Elsevier. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
16 | David Pereira, Nelma Moreira |
KAT and PHL in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Sci. Inf. Syst. ![In: Comput. Sci. Inf. Syst. 5(2), pp. 137-160, 2008. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Formaliz. Reason. ![In: J. Formaliz. Reason. 1(1), pp. 25-37, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
16 | Yves Bertot, Ekaterina Komendantskaya |
Inductive and Coinductive Components of Corecursive Functions in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/0807.1524, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP BibTeX RDF |
|
16 | Jean-François Dufourd |
Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/0802.2853, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP BibTeX RDF |
|
16 | Yves Bertot |
Structural abstract interpretation, A formal study using Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/0810.2179, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP BibTeX RDF |
|
16 | Russell O'Connor |
Certified Exact Transcendental Real Number Computation in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/0805.2438, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP BibTeX RDF |
|
16 | Nicolas Magaud, Julien Narboux, Pascal Schreck |
Formalizing Projective Plane Geometry in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry - 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008. Revised Papers, pp. 141-162, 2008, Springer, 978-3-642-21045-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
16 | Loic Pottier |
Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR Workshops ![In: Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008, 2008, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP BibTeX RDF |
|
16 | Jean-François Dufourd |
Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STACS ![In: STACS 2008, 25th Annual Symposium on Theoretical Aspects of Computer Science, Bordeaux, France, February 21-23, 2008, Proceedings, pp. 253-264, 2008, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
16 | Yves Bertot, Vladimir Komendantsky |
Fixed point semantics and partial recursion in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 15-17, 2008, Valencia, Spain, pp. 89-96, 2008, ACM, 978-1-60558-117-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Math. Struct. Comput. Sci. ![In: Math. Struct. Comput. Sci. 17(1), pp. 99-127, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
16 | Houda Anoun |
Une bibliothèque Coq pour le traitement des langues naturelles. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Tech. Sci. Informatiques ![In: Tech. Sci. Informatiques 26(9), pp. 1111-1136, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
16 | Matthieu Sozeau |
Program-ing finger trees in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pp. 13-24, 2007, ACM, 978-1-59593-815-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
16 | Brian E. Aydemir, Aaron Bohannon, Stephanie Weirich |
Nominal Reasoning Techniques in Coq: (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP@FLoC ![In: Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006, pp. 69-77, 2006, Elsevier. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Yves Bertot |
Coq in a Hurry ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/cs/0603118, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP BibTeX RDF |
|
16 | Laurent Théry |
Formalising Sylow's theorems in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/cs/0611057, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP BibTeX RDF |
|
16 | Yves Bertot |
CoInduction in Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/cs/0603119, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP BibTeX RDF |
|
16 | Laurent Théry, Pierre Letouzey, Georges Gonthier |
Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
The Seventeen Provers of the World ![In: The Seventeen Provers of the World, Foreword by Dana S. Scott, pp. 28-35, 2006, Springer, 3-540-30704-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Jacek Chrzaszcz, Jean-Pierre Jouannaud |
From OBJ to ML to Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Essays Dedicated to Joseph A. Goguen ![In: Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, pp. 216-234, 2006, Springer, 3-540-35462-X. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Jean-Pierre Jouannaud, Weiwen Xu |
Automatic Complexity Analysis for Programs Extracted from Coq Proof. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CLASE ![In: Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering, CLASE 2005, Edinburgh, UK, April 9, 2005, pp. 35-53, 2005, Elsevier. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Tech. Sci. Informatiques ![In: Tech. Sci. Informatiques 24(9), pp. 1113-1138, 2005. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Tech. Sci. Informatiques ![In: Tech. Sci. Informatiques 24(9), pp. 1139-1160, 2005. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/cs/0510011, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP BibTeX RDF |
|
16 | Russell O'Connor |
Essential Incompleteness of Arithmetic Verified by Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/cs/0505034, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP BibTeX RDF |
|
16 | David Delahaye, Micaela Mayero |
Dealing with algebraic expressions over a field in Coq using Maple. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Symb. Comput. ![In: J. Symb. Comput. 39(5), pp. 569-592, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Assia Mahboubi |
Programming and certifying a CAD algorithm in the Coq system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Mathematics, Algorithms, Proofs ![In: Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP BibTeX RDF |
|
16 | Reynald Affeldt, Naoki Kobayashi 0001 |
A Coq Library for Verification of Concurrent Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFM@IJCAR ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, LFM@IJCAR 2004. Cork, Ireland, July 5, 2004, pp. 17-32, 2004, Elsevier. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Christophe Dehlinger, Jean-François Dufourd |
Formalizing the trading theorem in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 323(1-3), pp. 399-442, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Christophe Dehlinger, Jean-François Dufourd |
Formalizing generalized maps in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 323(1-3), pp. 351-397, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Yves Bertot, Pierre Castéran |
Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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é. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2004 |
RDF |
|
16 | Martijn Oostdijk, Herman Geuvers |
Proof by computation in the Coq system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 272(1-2), pp. 293-314, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
16 | Dimitri Hendriks |
Proof Reflection in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 29(3-4), pp. 277-307, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
16 | Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg |
A Constructive Algebraic Hierarchy in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Symb. Comput. ![In: J. Symb. Comput. 34(4), pp. 271-286, 2002. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JFLA ![In: Journées francophones des langages applicatifs (JFLA'01), Pontarlier, France, Janvier, 2001, pp. 1-16, 2001, INRIA, 2-7261-1154-8. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP BibTeX RDF |
|
16 | David Delahaye, Micaela Mayero |
Field, une procédure de décision pour les nombres réels en Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JFLA ![In: Journées francophones des langages applicatifs (JFLA'01), Pontarlier, France, Janvier, 2001, pp. 33-48, 2001, INRIA, 2-7261-1154-8. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP BibTeX RDF |
|
16 | Laurent Chicli |
Une formalisation des faisceaux et des schémas affines en théorie des types avec Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JFLA ![In: Journées francophones des langages applicatifs (JFLA'01), Pontarlier, France, Janvier, 2001, pp. 17-32, 2001, INRIA, 2-7261-1154-8. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP BibTeX RDF |
|
16 | Pierre Letouzey, Laurent Théry |
Formalizing Stålmarck's Algorithm in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 388-405, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 23(3-4), pp. 319-346, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Kok Meng Yew, M. Zahidur Rahman, Sai Peck Lee |
Formal Verification of Secret Sharing Protocol Using Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASIAN ![In: Advances in Computing Science - ASIAN'99, 5th Asian Computing Science Conference, Phuket, Thailand, December 10-12, 1999, Proceedings, pp. 381-382, 1999, Springer, 3-540-66856-X. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Barbara Heyd, Pierre Crégut |
A Modular Coding of UNITY in COQ. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 251-266, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Solange Coupet-Grimal, Line Jakubiec |
Coq and Hardware Verification: A Case Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 125-139, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Bruno Barras |
Verification of the Interface of a Small Proof System in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'96, Aussois, France, December 15-19, 1996, Selected Papers, pp. 28-45, 1996, Springer, 3-540-65137-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Jean-François Monin |
Proving a Real Time Algorithm for ATM in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'96, Aussois, France, December 15-19, 1996, Selected Papers, pp. 277-293, 1996, Springer, 3-540-65137-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Delphine Terrasse |
Encoding Natural Semantics in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 4th International Conference, AMAST '95, Montreal, Canada, July 3-7, 1995, Proceedings, pp. 230-244, 1995, Springer, 3-540-60043-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings, pp. 312-327, 1995, Springer, 3-540-59048-X. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Joëlle Despeyroux, Amy P. Felty, André Hirschowitz |
Higher-Order Abstract Syntax in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings, pp. 124-138, 1995, Springer, 3-540-59048-X. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Cristina Cornes, Delphine Terrasse |
Automating Inversion of Inductive Predicates in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, pp. 85-104, 1995, Springer, 3-540-61780-9. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Eduardo Giménez 0001 |
An Application of Co-inductive Types in Coq: Verification of the Alternating Bit Protocol. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, pp. 135-152, 1995, Springer, 3-540-61780-9. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Amokrane Saïbi |
Formalization of a lamda-Calculus with Explicit Substitutions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, pp. 183-202, 1994, Springer, 3-540-60579-7. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
16 | Christine Paulin-Mohring, Benjamin Werner |
Synthesis of ML Programs in the System Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Symb. Comput. ![In: J. Symb. Comput. 15(5/6), pp. 607-640, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
16 | Christine Paulin-Mohring |
Inductive Definitions in the system Coq - Rules and Properties. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, pp. 328-345, 1993, Springer, 3-540-56517-5. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
16 | Catherine Parent |
Developing Certified Programs in the System Coq - The Program Tactic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, pp. 291-312, 1993, Springer, 3-540-58085-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
16 | François Leclerc, Christine Paulin-Mohring |
Programming with Streams in Coq - A Case Study: the Sieve of Eratosthenes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, pp. 191-212, 1993, Springer, 3-540-58085-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
11 | Limin Jia 0001, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich |
Dependent types and program equivalence. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pp. 275-286, 2010, ACM, 978-1-60558-479-9. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
dependent types, program equivalence |
11 | Aquinas Hobor, Robert Dockins, Andrew W. Appel |
A theory of indirection via approximation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pp. 171-184, 2010, ACM, 978-1-60558-479-9. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
indirection theory, step-indexed models |
11 | Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine |
Structuring the verification of heap-manipulating programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pp. 261-274, 2010, ACM, 978-1-60558-479-9. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
type theory, monads, hoare logic, separation logic |
11 | Andreas Rossberg, Claudio V. Russo, Derek Dreyer |
F-ing modules. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLDI ![In: Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010, pp. 89-102, 2010, ACM, 978-1-60558-891-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 58(2), pp. 220-225, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Xavier Leroy |
Formal verification of a realistic compiler. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Commun. ACM ![In: Commun. ACM 52(7), pp. 107-115, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Hugo Herbelin, Gyesik Lee |
Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WoLLIC ![In: Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings, pp. 209-217, 2009, Springer, 978-3-642-02260-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings, pp. 541-560, 2009, Springer, 978-3-642-10372-8. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Keiko Nakata 0001, Tarmo Uustalu |
Trace-Based Coinductive Operational Semantics for While. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 375-390, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Wouter Swierstra |
A Hoare Logic for the State Monad. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 440-451, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Dabrowski, David Pichardie |
A Certified Data Race Analysis for a Java-like Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 212-227, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Nicolas Julien, Ioana Pasca |
Formal Verification of Exact Computations Using Newton's Method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 408-423, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Andrew McCreight |
Practical Tactics for Separation Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 343-358, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Robert Atkey |
Syntax for Free: Representing Syntax with Binding Using Parametricity. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, pp. 35-49, 2009, Springer, 978-3-642-02272-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, pp. 275-293, 2009, Springer, 978-3-642-10671-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Robert Dockins, Aquinas Hobor, Andrew W. Appel |
A Fresh Look at Separation Algebras and Share Accounting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, pp. 161-177, 2009, Springer, 978-3-642-10671-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Richard Dapoigny, Patrick Barlatier |
Towards an Ontological Modeling with Dependent Types: Application to Part-Whole Relations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ER ![In: Conceptual Modeling - ER 2009, 28th International Conference on Conceptual Modeling, Gramado, Brazil, November 9-12, 2009. Proceedings, pp. 145-158, 2009, Springer, 978-3-642-04839-5. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Yuan Dong, Shengyuan Wang, Liwei Zhang, Ping Yang |
Modular Certification of Low-Level Intermediate Representation Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COMPSAC (1) ![In: Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference, COMPSAC 2009, Seattle, Washington, USA, July 20-24, 2009. Volume 1, pp. 563-570, 2009, IEEE Computer Society, 978-0-7695-3726-9. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Benjamin C. Pierce |
Lambda, the ultimate TA: using a proof assistant to teach programming language foundations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009, pp. 121-122, 2009, ACM, 978-1-60558-332-7. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
programming languages, pedagogy, proof assistants |
11 | Nick Benton, Chung-Kil Hur |
Biorthogonality, step-indexing and compiler correctness. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009, pp. 97-108, 2009, ACM, 978-1-60558-332-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESEC/SIGSOFT FSE ![In: Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009, Amsterdam, The Netherlands, August 24-28, 2009, pp. 243-252, 2009, ACM, 978-1-60558-001-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOAL ![In: Proceedings of the 8th Workshop on Foundations of Aspect-Oriented Languages, FOAL 2009, Charlottesville, Virginia, USA, March 2, 2009, pp. 31-35, 2009, ACM, 978-1-60558-452-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLDI ![In: Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, pp. 3-14, 2009, ACM, 978-1-60558-420-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, pp. 83-92, 2009, ACM, 978-1-60558-568-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2009, 12th International Conference, Las Palmas de Gran Canaria, Spain, February 15-20, 2009, Revised Selected Papers, pp. 203-210, 2009, Springer, 978-3-642-04771-8. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie |
Certified Static Analysis by Abstract Interpretation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOSAD ![In: Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, pp. 223-257, 2009, Springer, 978-3-642-03828-0. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|