2. ITP 2011: Berg en Dal, The Netherlands

Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk (Eds.): 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

- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Batory11
- ask others
Don S. Batory: Towards Verification of Product Lines. 1
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Gonthier11
- ask others
Georges Gonthier: Advances in the Formalization of the Odd Order Theorem. 2
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/JacobsS11
- ask others
Bart Jacobs, Ronny Wichers Schreur: Logical Formalisation and Analysis of the Mifare Classic Card in PVS. 3-17
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/KishinevskyGV11
- ask others
Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov: Challenges in Verifying Communication Fabrics. 18-21

Regular Papers

- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/BengtsonJSB11
- ask others
Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal: Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. 22-38
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Beringer11
- ask others
Lennart Beringer: Relational Decomposition. 39-54
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/BosserCFC11
- ask others
Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza: Structural Analysis of Narratives with the Coq Proof Assistant. 55-70
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/ClavelPL11
- ask others
Renaud Clavel, Laurence Pierre, Régis Leveugle: Towards Robustness Analysis Using PVS. 71-86
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Gammie11
- ask others
Peter Gammie: Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. 87-102
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Gonthier11a
- ask others
Georges Gonthier: Point-Free, Set-Free Concrete Linear Algebra. 103-118
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/HeraudN11
- ask others
Sylvain Heraud, David Nowak: A Formalization of Polytime Functions. 119-134
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/HolzlH11
- ask others
Johannes Hölzl, Armin Heller: Three Chapters of Measure Theory in Isabelle/HOL. 135-151
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/KraussSTFG11
- ask others
Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl: Termination of Isabelle Functions via Termination of Rewriting. 152-167
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/KumarW11
- ask others
Ramana Kumar, Tjark Weber: Validating QBF Validity in HOL4. 168-183
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Kuncar11
- ask others
Ondrej Kuncar: Proving Valid Quantified Boolean Formulas in HOL Light. 184-199
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/LambanMRR11
- ask others
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
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/LochbihlerB11
- ask others
Andreas Lochbihler, Lukas Bulwahn: Animating the Formalised Semantics of a Java-Like Language. 216-232
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/MhamdiHT11
- ask others
Tarek Mhamdi, Osman Hasan, Sofiène Tahar: Formalization of Entropy Measures in HOL. 233-248
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/MonniauxC11
- ask others
David Monniaux, Pierre Corbineau: On the Generation of Positivstellensatz Witnesses in Degenerate Cases. 249-264
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/MyreenD11
- ask others
Magnus O. Myreen, Jared Davis: A Verified Runtime for a Verified Theorem Prover. 265-280
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Nipkow11
- ask others
Tobias Nipkow: Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. 281-296
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Norrish11
- ask others
Michael Norrish: Mechanised Computability Theory. 297-311
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/ReidG11
- ask others
Peter Reid, Ruben Gamboa: Automatic Differentiation in ACL2. 312-324
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/SewellWGMAK11
- ask others
Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein: seL4 Enforces Integrity. 325-340

Proof Pearls

- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/WuZU11
- ask others
Chunhan Wu, Xingyuan Zhang, Christian Urban: A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). 341-356

Rough Diamonds

- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/Fox11
- ask others
Anthony C. J. Fox: LCF-Style Bit-Blasting in HOL4. 357-362
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/OwensBNS11
- ask others
Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell: Lem: A Lightweight Tool for Heavyweight Semantics. 363-369
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/ScottF11
- ask others
Phil Scott, Jacques D. Fleuriot: Composable Discovery Engines for Interactive Theorem Proving. 370-375
- view
  - electronic edition @ doi.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/itp/UrbasJ11
- ask others
Matej Urbas, Mateja Jamnik: Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers. 376-382