Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
44 | Johannes Hölzl |
Markov processes in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 100-111, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Xinyu Feng 0001 |
Mechanized verification of preemptive OS kernels (invited talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 2, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002 |
A formalization of the Berlekamp-Zassenhaus factorization algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 17-29, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Lawrence C. Paulson |
Porting the HOL light analysis library: some lessons (invited talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 1, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong |
Complx: a verification framework for concurrent imperative programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 138-150, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti |
Verifying dynamic race detection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 151-163, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Reynald Affeldt, Cyril Cohen |
Formal foundations of 3D geometry to model robot manipulators. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 30-42, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters |
The HoTT library: a formalization of homotopy type theory in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 164-172, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Érik Martin-Dorel, Pierre Roux |
A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 90-99, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | François Pottier |
Verifying a hash table and its iterators in higher-order separation logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 3-16, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Gaëtan Gilbert |
Formalising real numbers in homotopy type theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 112-124, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Jonas Kaiser, Tobias Tebbi, Gert Smolka |
Equivalence of system f and ź2 in Coq based on context morphism lemmas. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 222-234, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau |
The next 700 syntactical models of type theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 182-194, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Jan Jakubuv, Josef Urban |
BliStrTune: hierarchical invention of theorem proving strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 43-52, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Guillaume Allais, James Chapman 0001, Conor McBride, James McKinna |
Type-and-scope safe programs and their proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 195-207, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar |
Verified compilation of CakeML to multiple machine-code targets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 125-137, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero |
A Coq formal proof of the LaxMilgram theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 79-89, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto |
Formalization of Karp-Miller tree construction on petri nets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 66-78, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Jesper Cockx, Dominique Devriese |
Lifting proof-relevant unification to higher dimensions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 173-181, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Reuben N. S. Rowe, James Brotherston |
Automatic cyclic termination proofs for recursive procedures in separation logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pp. 53-65, 2017, ACM, 978-1-4503-4705-1. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
44 | Xavier Leroy, Alwen Tiu (eds.) |
Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015 ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![ACM, 978-1-4503-3296-5 The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP BibTeX RDF |
|
44 | Andrea Asperti |
The Speedup Theorem in a Primitive Recursive Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 175-182, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu |
A Compositional Semantics for Verified Separate Compilation and Linking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 3-14, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Steven Schäfer, Gert Smolka, Tobias Tebbi |
Completeness and Decidability of de Bruijn Substitution Algebra in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 67-73, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Yves Bertot |
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 147-155, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Ondrej Kuncar |
Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 85-94, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Martin Bodin, Thomas P. Jensen, Alan Schmitt |
Certified Abstract Interpretation with Pretty-Big-Step Semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 29-40, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Zhong Shao |
Clean-Slate Development of Certified OS Kernels. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 95-96, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Xiao Jia 0001, Wei Li, Viktor Vafeiadis |
Proving Lock-Freedom Easily and Automatically. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 119-127, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Manuel Eberl |
A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 75-83, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Kaustuv Chaudhuri, Matteo Cimini, Dale Miller 0001 |
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 157-166, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Denis Firsov, Tarmo Uustalu |
Certified Normalization of Context-Free Grammars. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 167-174, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Sandrine Blazy, André Maroneze, David Pichardie |
Verified Validation of Program Slicing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 109-117, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Fabian Immler |
A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 129-136, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Robbert Krebbers, Freek Wiedijk |
A Typed C11 Semantics for Interactive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 15-27, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Thomas Sternagel, Sarah Winkler, Harald Zankl |
Recording Completion for Certificates in Equational Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 41-47, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Jingyuan Cao, Ming Fu, Xinyu Feng 0001 |
Practical Tactics for Verifying C Programs in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 97-108, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Viktor Vafeiadis |
Formal Reasoning about the C11 Weak Memory Model. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 1-2, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Cezary Kaliszyk, Josef Urban, Jirí Vyskocil |
Certified Connection Tableaux Proofs for HOL Light and TPTP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 59-66, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Peter Lammich, René Neumann |
A Framework for Verifying Depth-First Search Algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 137-146, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Thibault Gauthier, Cezary Kaliszyk |
Premise Selection and External Provers for HOL4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 49-57, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
44 | Georges Gonthier, Michael Norrish (eds.) |
Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![Springer, 978-3-319-03544-4 The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Brian Huffman, Ondrej Kuncar |
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. ![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. 131-146, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | 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 |
|
44 | Andrea Asperti |
A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem. ![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. 163-177, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Daniel Huang 0001, Greg Morrisett |
Formalizing the SAFECode Type System. ![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. 211-226, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Denis Firsov, Tarmo Uustalu |
Certified Parsing of Regular Languages. ![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. 98-113, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka |
Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. ![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. 243-258, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Cyril Cohen, Maxime Dénès, Anders Mörtberg |
Refinements for Free! ![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. 147-162, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Christian Sternagel |
Certified Kruskal's Tree Theorem. ![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. 178-193, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | 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 |
|
44 | Christian J. Bell |
Certifiably Sound Parallelizing Transformations. ![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. 227-242, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Daniel R. Licata, Guillaume Brunerie |
π n (S n ) in Homotopy Type Theory. ![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. 1-16, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Dale Miller 0001, Alwen Tiu |
Extracting Proofs from Tabled Proof Search. ![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. 194-210, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Andrei Popescu 0001, Johannes Hölzl, Tobias Nipkow |
Formalizing Probabilistic Noninterference. ![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. 259-275, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Magnus O. Myreen, Gregorio Curello |
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. ![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. 66-81, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | 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 |
|
44 | Narges Khakpour, Oliver Schwarz, Mads Dam |
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties. ![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. 276-291, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Chunhan Wu, Xingyuan Zhang, Christian Urban |
A Formal Model and Correctness Proof for an Access Control Policy Framework. ![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. 292-307, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Josiah Dodds, Andrew W. Appel |
Mostly Sound Type System Improves a Foundational Program Verifier. ![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. 17-32, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Andreas Schropp, Andrei Popescu 0001 |
Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. ![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. 114-130, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
44 | Chris Hawblitzel, Dale Miller 0001 (eds.) |
Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![Springer, 978-3-642-35307-9 The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Andrei Popescu 0001, Johannes Hölzl, Tobias Nipkow |
Proving Concurrent Noninterference. ![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. 109-125, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Christian Doczkal, Gert Smolka |
Constructive Completeness for Modal Logic with Transitive Closure. ![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. 224-239, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Naoki Kobayashi 0001 |
Program Certification by Higher-Order Model Checking. ![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. 9-10, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Pierre Neron |
A Formal Proof of Square Root and Division Elimination in Embedded Programs. ![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. 256-272, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Lukas Bulwahn |
The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. ![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. 92-108, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Alexander Vaynberg, Zhong Shao |
Compositional Verification of a Baby Virtual Memory Manager. ![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. 143-159, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Dominic P. Mulligan, Claudio Sacerdoti Coen |
On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor. ![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. 43-59, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Xavier Leroy |
Mechanized Semantics for Compiler Verification. ![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. 4-6, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | 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 |
|
44 | Jianzhou Zhao, Steve Zdancewic |
Mechanized Verification of Computing Dominators for Formalizing Compilers. ![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. 27-42, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein |
Noninterference for Operating System Kernels. ![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. 126-142, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Greg Morrisett |
Scalable Formal Machine Models. ![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. 1-3, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Thierry Coquand, Anders Mörtberg, Vincent Siles |
Coherent and Strongly Discrete Rings in Type Theory. ![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. 273-288, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Kaustuv Chaudhuri |
Compact Proof Certificates for Linear Logic. ![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. 208-223, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Hing-Lun Chan, Michael Norrish |
A String of Pearls: Proofs of Fermat's Little Theorem. ![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. 188-207, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Keisuke Nakano 0001 |
Shall We Juggle, Coinductively? ![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. 160-172, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin |
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. ![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. 7-8, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Brian Campbell 0001 |
An Executable Semantics for CompCert C. ![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. 60-75, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Andrea Asperti, Wilmer Ricciotti |
Rating Disambiguation Errors. ![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. 240-255, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois |
Producing Certified Functional Code from Inductive Specifications. ![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. 76-91, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Valentin Robert, Xavier Leroy |
A Formally-Verified Alias Analysis. ![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. 11-26, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Beniamino Accattoli |
Proof Pearl: Abella Formalization of λ-Calculus Cube Property. ![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. 173-187, 2012, Springer, 978-3-642-35307-9. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
44 | Jean-Pierre Jouannaud, Zhong Shao (eds.) |
Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![Springer, 978-3-642-25378-2 The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | Tom Ridge |
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars. ![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. 103-118, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | James Cheney, Christian Urban |
Mechanizing the Metatheory of mini-XQuery. ![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. 280-295, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire |
Full Reduction at Full Throttle. ![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. 362-377, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | Sorin Stratulat, Vincent Demange |
Automated Certification of Implicit Induction Proofs. ![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. 37-53, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | Thierry Coquand, Vincent Siles |
A Decision Procedure for Regular Expression Equivalence in Type Theory. ![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. 119-134, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | Michael Backes 0001, Catalin Hritcu, Thorsten Tarrach |
Automatically Verifying Typing Constraints for a Data Processing Language. ![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. 296-313, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui |
First Steps towards the Certification of an ARM Simulator Using Compcert. ![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. 346-361, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | 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 |
|
44 | Andrew W. Appel |
VeriSmall: Verified Smallfoot Shape Analysis. ![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. 231-246, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | Christian Doczkal, Gert Smolka |
Constructive Formalization of Hybrid Logic with Eventualities. ![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. 5-20, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | 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 |
|
44 | Nikolaj S. Bjørner |
Engineering Theories with Z3. ![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. 1-2, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
44 | 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 |
|
44 | 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 |
|
44 | Frank Pfenning, Luís Caires, Bernardo Toninho |
Proof-Carrying Code in a Session-Typed Process Calculus. ![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. 21-36, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|