default search action

combined dblp search
author search
venue search
publication search

ask others

3. ITP 2012: Princeton, NJ, USA

> Home > Conferences and Workshops > ITP

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  authority control:
- export record
  dblp key:
  - conf/itp/2012
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/2012
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

- view
  authority control:
- export record
  dblp key:
  - conf/itp/Paulson12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Paulson12
Lawrence C. Paulson:
MetiTarski: Past and Future. 1-10
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BartheCGKB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BartheCGKB12
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin:
Computer-Aided Cryptographic Proofs. 11-27
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Platzer12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Platzer12
André Platzer:
A Differential Operator Approach to Equational Differential Invariants - (Invited Paper). 28-48

Invited Tutorial

- view
  authority control:
- export record
  dblp key:
  - conf/itp/Gacek12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Gacek12
Andrew Gacek:
Abella: A Tutorial. 49-50

Formalization of Mathematics I

- view
  authority control:
- export record
  dblp key:
  - conf/itp/GamboaC12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/GamboaC12
Ruben Gamboa, John R. Cowles:
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. 51-66
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Cohen12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Cohen12
Cyril Cohen:
Construction of Real Algebraic Numbers in Coq. 67-82
- view
  authority control:
- export record
  dblp key:
  - conf/itp/DenesMS12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/DenesMS12
Maxime Dénès, Anders Mörtberg, Vincent Siles:
A Refinement-Based Approach to Computational Algebra in Coq. 83-98

Program Abstraction and Logics

- view
  authority control:
- export record
  dblp key:
  - conf/itp/GreenawayAK12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/GreenawayAK12
David Greenaway, June Andronick, Gerwin Klein:
Bridging the Gap: Automatic Verified Abstraction of C. 99-115
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Nipkow12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Nipkow12
Tobias Nipkow:
Abstract Interpretation of Annotated Commands. 116-132
- view
  authority control:
- export record
  dblp key:
  - conf/itp/MichelP12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/MichelP12
Patrick Michel, Arnd Poetzsch-Heffter:
Verifying and Generating WP Transformers for Procedures on Complex Data. 133-148

Data Structures and Synthesis

- view
  authority control:
- export record
  dblp key:
  - conf/itp/Danielsson12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Danielsson12
Nils Anders Danielsson:
Bag Equivalence via a Proof-Relevant Membership Relation. 149-165
- view
  authority control:
- export record
  dblp key:
  - conf/itp/LammichT12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/LammichT12
Peter Lammich, Thomas Tuerk:
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. 166-182
- view
  authority control:
- export record
  dblp key:
  - conf/itp/MiculanP12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/MiculanP12
Marino Miculan, Marco Paviotti:
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. 183-200

Security

- view
  authority control:
- export record
  dblp key:
  - conf/itp/BaeldeCGP12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BaeldeCGP12
David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring:
Towards Provably Robust Watermarking. 201-216
- view
  authority control:
- export record
  dblp key:
  - conf/itp/ZhangUW12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/ZhangUW12
Xingyuan Zhang, Christian Urban, Chunhan Wu:
Priority Inheritance Protocol Proved Correct. 217-232
- view
  authority control:
- export record
  dblp key:
  - conf/itp/AffeldtH12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/AffeldtH12
Reynald Affeldt, Manabu Hagiwara:
Formalization of Shannon's Theorems in SSReflect-Coq. 233-249

(Non-)Termination and Automata

- view
  authority control:
- export record
  dblp key:
  - conf/itp/VytiniotisCW12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/VytiniotisCW12
Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt:
Stop When You Are Almost-Full - Adventures in Constructive Termination. 250-265
- view
  authority control:
- export record
  dblp key:
  - conf/itp/SternagelT12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/SternagelT12
Christian Sternagel, René Thiemann:
Certification of Nontermination Proofs. 266-282
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Asperti12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Asperti12
Andrea Asperti:
A Compact Proof of Decidability for Regular Expression Equivalence. 283-298

Program Verification

- view
  authority control:
- export record
  dblp key:
  - conf/itp/ManskyG12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/ManskyG12
William Mansky, Elsa L. Gunter:
Using Locales to Define a Rely-Guarantee Temporal Logic. 299-314
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BengtsonJB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BengtsonJB12
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

- view
  authority control:
- export record
  dblp key:
  - conf/itp/KleinKB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KleinKB12
Gerwin Klein, Rafal Kolanski, Andrew Boyton:
Mechanised Separation Algebra. 332-337
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Fox12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Fox12
Anthony C. J. Fox:
Directions in ISA Specification. 338-344

Theorem Prover Development

- view
  authority control:
- export record
  dblp key:
  - conf/itp/BlanchettePWW12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BlanchettePWW12
Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach:
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. 345-360
- view
  authority control:
- export record
  dblp key:
  - conf/itp/GonthierT12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/GonthierT12
Georges Gonthier, Enrico Tassi:
A Language of Patterns for Subterm Selection. 361-376

Formalization of Mathematics II

- view
  authority control:
- export record
  dblp key:
  - conf/itp/ImmlerH12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/ImmlerH12
Fabian Immler, Johannes Hölzl:
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. 377-392
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Noschinski12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Noschinski12
Lars Noschinski:
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem. 393-404

Rough Diamonds II: Prover Infrastructure and Modeling Styles

- view
  authority control:
- export record
  dblp key:
  - conf/itp/KumarH12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KumarH12
Ramana Kumar, Joe Hurd:
Standalone Tactics Using OpenTheory. 405-411
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Myreen12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Myreen12
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.