default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID2. ITP 2011: Berg en Dal, The Netherlands
- Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk:
Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings. Lecture Notes in Computer Science 6898, Springer 2011, ISBN 978-3-642-22862-9
Invited Papers
- Don S. Batory:
Towards Verification of Product Lines. 1 - Georges Gonthier:
Advances in the Formalization of the Odd Order Theorem. 2 - Bart Jacobs, Ronny Wichers Schreur:
Logical Formalisation and Analysis of the Mifare Classic Card in PVS. 3-17 - Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov:
Challenges in Verifying Communication Fabrics. 18-21
Regular Papers
- Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski
, Lars Birkedal:
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. 22-38 - Lennart Beringer:
Relational Decomposition. 39-54 - Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza:
Structural Analysis of Narratives with the Coq Proof Assistant. 55-70 - Renaud Clavel, Laurence Pierre, Régis Leveugle:
Towards Robustness Analysis Using PVS. 71-86 - Peter Gammie:
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. 87-102 - Georges Gonthier:
Point-Free, Set-Free Concrete Linear Algebra. 103-118 - Sylvain Heraud, David Nowak:
A Formalization of Polytime Functions. 119-134 - Johannes Hölzl, Armin Heller:
Three Chapters of Measure Theory in Isabelle/HOL. 135-151 - Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl:
Termination of Isabelle Functions via Termination of Rewriting. 152-167 - Ramana Kumar, Tjark Weber:
Validating QBF Validity in HOL4. 168-183 - Ondrej Kuncar:
Proving Valid Quantified Boolean Formulas in HOL Light. 184-199 - Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina:
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. 200-215 - Andreas Lochbihler, Lukas Bulwahn:
Animating the Formalised Semantics of a Java-Like Language. 216-232 - Tarek Mhamdi, Osman Hasan, Sofiène Tahar:
Formalization of Entropy Measures in HOL. 233-248 - David Monniaux, Pierre Corbineau:
On the Generation of Positivstellensatz Witnesses in Degenerate Cases. 249-264 - Magnus O. Myreen, Jared Davis:
A Verified Runtime for a Verified Theorem Prover. 265-280 - Tobias Nipkow:
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. 281-296 - Michael Norrish:
Mechanised Computability Theory. 297-311 - Peter Reid, Ruben Gamboa:
Automatic Differentiation in ACL2. 312-324 - Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein:
seL4 Enforces Integrity. 325-340
Proof Pearls
- Chunhan Wu, Xingyuan Zhang, Christian Urban:
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). 341-356
Rough Diamonds
- Anthony C. J. Fox:
LCF-Style Bit-Blasting in HOL4. 357-362 - Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell:
Lem: A Lightweight Tool for Heavyweight Semantics. 363-369 - Phil Scott, Jacques D. Fleuriot:
Composable Discovery Engines for Interactive Theorem Proving. 370-375 - Matej Urbas, Mateja Jamnik:
Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers. 376-382
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-12-04 22:07 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
