Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio 0001, José-Luis Ruiz-Reina |
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. ![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. 200-215, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Peter Reid, Ruben Gamboa |
Automatic Differentiation in ACL2. ![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. 312-324, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Peter Gammie |
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. ![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. 87-102, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Johannes Hölzl, Armin Heller |
Three Chapters of Measure Theory in Isabelle/HOL. ![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. 135-151, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Tarek Mhamdi, Osman Hasan, Sofiène Tahar |
Formalization of Entropy Measures in HOL. ![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. 233-248, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Ramana Kumar, Tjark Weber |
Validating QBF Validity in HOL4. ![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. 168-183, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Sylvain Heraud, David Nowak |
A Formalization of Polytime Functions. ![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. 119-134, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Matej Urbas, Mateja Jamnik |
Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers. ![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. 376-382, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Phil Scott, Jacques D. Fleuriot |
Composable Discovery Engines for Interactive Theorem Proving. ![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. 370-375, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Ondrej Kuncar |
Proving Valid Quantified Boolean Formulas in HOL Light. ![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. 184-199, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Krauss 0001, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl |
Termination of Isabelle Functions via Termination of Rewriting. ![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. 152-167, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Lennart Beringer |
Relational Decomposition. ![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. 39-54, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Anthony C. J. Fox |
LCF-Style Bit-Blasting in HOL4. ![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. 357-362, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein |
seL4 Enforces Integrity. ![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. 325-340, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov |
Challenges in Verifying Communication Fabrics. ![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. 18-21, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | David Monniaux, Pierre Corbineau |
On the Generation of Positivstellensatz Witnesses in Degenerate Cases. ![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. 249-264, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Georges Gonthier |
Advances in the Formalization of the Odd Order Theorem. ![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. 2, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Tobias Nipkow |
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. ![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. 281-296, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Renaud Clavel, Laurence Pierre, Régis Leveugle |
Towards Robustness Analysis Using PVS. ![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. 71-86, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Jasmin Christian Blanchette, Tobias Nipkow |
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 131-146, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Panagiotis Manolios, Daron Vroon 0001 |
Interactive Termination Proofs Using Termination Cores. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 355-370, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Anthony C. J. Fox, Magnus O. Myreen |
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 243-258, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | David Cachera, David Pichardie |
A Certified Denotational Abstract Interpreter. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 9-24, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Gerwin Klein |
A Formally Verified OS Kernel. Now What? ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 1-7, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Freek Verbeek, Julien Schmaltz |
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 67-82, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Sol Swords, Warren A. Hunt Jr. |
A Mechanically Verified AIG-to-BDD Conversion Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 435-449, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Magnus O. Myreen |
Separation Logic Adapted for Proofs by Rewriting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 485-489, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Matthieu Sozeau |
Equations: A Dependent Pattern-Matching Compiler. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 419-434, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Benjamin C. Pierce |
Proof Assistants as Teaching Assistants: A View from the Trenches. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 8, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Sascha Böhme, Tjark Weber |
Fast LCF-Style Proof Reconstruction for Z3. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 179-194, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Joe Hendrix, Deepak Kapur, José Meseguer 0001 |
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 275-290, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Ernie Cohen, Bert Schirmer |
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 403-418, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Serge Autexier, Dominik Dietrich |
A Tactic Language for Declarative Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 99-114, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen |
Automated Machine-Checked Hybrid System Safety Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 259-274, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty, Brigitte Pientka |
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 227-242, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Krauss 0001, Andreas Schropp |
A Mechanized Translation from Higher-Order Logic to Set Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 323-338, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Moa Johansson, Lucas Dixon, Alan Bundy |
Case-Analysis for Rippling and Inductive Proof. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 291-306, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | William Mansky, Elsa L. Gunter |
A Framework for Formal Verification of Compiler Optimizations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 371-386, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz |
Inductive Consequences in the Calculus of Constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 450-465, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis |
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 147-162, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Jean-François Dufourd, Yves Bertot |
Formal Study of Plane Delaunay Triangulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 211-226, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Tjark Weber |
Validating QBF Invalidity in HOL4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 466-480, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Brian Huffman, Christian Urban |
A New Foundation for Nominal Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 35-50, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Tarek Mhamdi, Osman Hasan, Sofiène Tahar |
On the Formalization of the Lebesgue Integration Theory in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 387-402, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Ramana Kumar, Michael Norrish |
(Nominal) Unification by Recursive Descent with Triangular Substitutions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 51-66, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin |
Programming Language Techniques for Cryptographic Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 115-130, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Arthur Charguéraud |
The Optimal Fixed Point Combinator. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 195-210, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Peter Lammich, Andreas Lochbihler |
The Isabelle Collections Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 339-354, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | John R. Cowles, Ruben Gamboa |
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 25-34, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Matt Kaufmann, Lawrence C. Paulson (eds.) |
Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![Springer, 978-3-642-14051-8 The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Douglas J. Howe |
Higher-Order Abstract Syntax in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 481-484, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|