default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID3. ITP 2012: Princeton, NJ, USA
- Lennart Beringer, Amy P. Felty:
Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. Lecture Notes in Computer Science 7406, Springer 2012, ISBN 978-3-642-32346-1
Invited Talks
- Lawrence C. Paulson
:
MetiTarski: Past and Future. 1-10 - Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin:
Computer-Aided Cryptographic Proofs. 11-27 - André Platzer:
A Differential Operator Approach to Equational Differential Invariants - (Invited Paper). 28-48
Invited Tutorial
- Andrew Gacek:
Abella: A Tutorial. 49-50
Formalization of Mathematics I
- Ruben Gamboa, John R. Cowles:
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. 51-66 - Cyril Cohen:
Construction of Real Algebraic Numbers in Coq. 67-82 - Maxime Dénès, Anders Mörtberg, Vincent Siles:
A Refinement-Based Approach to Computational Algebra in Coq. 83-98
Program Abstraction and Logics
- David Greenaway, June Andronick, Gerwin Klein:
Bridging the Gap: Automatic Verified Abstraction of C. 99-115 - Tobias Nipkow:
Abstract Interpretation of Annotated Commands. 116-132 - Patrick Michel, Arnd Poetzsch-Heffter:
Verifying and Generating WP Transformers for Procedures on Complex Data. 133-148
Data Structures and Synthesis
- Nils Anders Danielsson:
Bag Equivalence via a Proof-Relevant Membership Relation. 149-165 - Peter Lammich, Thomas Tuerk:
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. 166-182 - Marino Miculan, Marco Paviotti:
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. 183-200
Security
- David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring:
Towards Provably Robust Watermarking. 201-216 - Xingyuan Zhang, Christian Urban, Chunhan Wu:
Priority Inheritance Protocol Proved Correct. 217-232 - Reynald Affeldt, Manabu Hagiwara:
Formalization of Shannon's Theorems in SSReflect-Coq. 233-249
(Non-)Termination and Automata
- Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt:
Stop When You Are Almost-Full - Adventures in Constructive Termination. 250-265 - Christian Sternagel, René Thiemann:
Certification of Nontermination Proofs. 266-282 - Andrea Asperti:
A Compact Proof of Decidability for Regular Expression Equivalence. 283-298
Program Verification
- William Mansky, Elsa L. Gunter:
Using Locales to Define a Rely-Guarantee Temporal Logic. 299-314 - Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal:
Charge! - A Framework for Higher-Order Separation Logic in Coq. 315-331
Rough Diamonds I: Reasoning about Program Execution
- Gerwin Klein, Rafal Kolanski, Andrew Boyton:
Mechanised Separation Algebra. 332-337 - Anthony C. J. Fox:
Directions in ISA Specification. 338-344
Theorem Prover Development
- Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach:
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. 345-360 - Georges Gonthier, Enrico Tassi:
A Language of Patterns for Subterm Selection. 361-376
Formalization of Mathematics II
- Fabian Immler, Johannes Hölzl:
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. 377-392 - Lars Noschinski:
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem. 393-404
Rough Diamonds II: Prover Infrastructure and Modeling Styles
- Ramana Kumar, Joe Hurd:
Standalone Tactics Using OpenTheory. 405-411 - Magnus O. Myreen:
Functional Programs: Conversions between Deep and Shallow Embeddings. 412-417
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-14 23:19 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:
