My Library

University LibraryCatalogue

For faster,
Use Lean
Get it now
Don't show me again
Limit search to items available for borrowing or consultation
Result Page: Previous Next
Can't find that book? Try BONUS+
Look for full text

Search Discovery

Search CARM Centre Catalogue

Search Trove

Add record to RefWorks

Cover Art
Author ITP (Conference) (3rd : 2012 : Princeton, N.J.)

Title Interactive theorem proving [electronic resource] : third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings / Lennart Beringer, Amy Felty (eds.).

Published Berlin ; New York : Springer, ©2012.


Location Call No. Status
Physical description 1 online resource (xi, 417 pages) : illustrations.
Series Lecture notes in computer science, 1611-3349 ; 7406
LNCS sublibrary. SL 1, Theoretical computer science and general issues
Lecture notes in computer science ; 7406. 1611-3349
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
Springer Lecture Notes in Computer Science
Notes International conference proceedings.
Contents MetiTarski: Past and Future / Lawrence C. Paulson -- Computer-Aided Cryptographic Proofs / Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz and Santiago Zanella Béguelin -- A Differential Operator Approach to Equational Differential Invariants (Invited Paper) / André Platzer -- Abella: A Tutorial / Andrew Gacek -- A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers / Ruben Gamboa and John Cowles -- Construction of Real Algebraic Numbers in Coq / Cyril Cohen -- A Refinement-Based Approach to Computational Algebra in Coq / Maxime Dénès, Anders Mörtberg and Vincent Siles -- Bridging the Gap: Automatic Verified Abstraction of C / David Greenaway, June Andronick and Gerwin Klein -- Abstract Interpretation of Annotated Commands / Tobias Nipkow -- Verifying and Generating WP Transformers for Procedures on Complex Data / Patrick Michel and Arnd Poetzsch-Heffter -- Bag Equivalence via a Proof-Relevant Membership Relation / Nils Anders Danielsson -- Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm / Peter Lammich and Thomas Tuerk -- Synthesis of Distributed Mobile Programs Using Monadic Types in Coq / Marino Miculan and Marco Paviotti -- Towards Provably Robust Watermarking / David Baelde, Pierre Courtieu, David Gross-Amblard and Christine Paulin-Mohring.
Priority Inheritance Protocol Proved Correct / Xingyuan Zhang, Christian Urban and Chunhan Wu -- Formalization of Shannon's Theorems in SSReflect-Coq / Reynald Affeldt and Manabu Hagiwara -- Stop When You Are Almost-Full: Adventures in Constructive Termination / Dimitrios Vytiniotis, Thierry Coquand and David Wahlstedt -- Certification of Nontermination Proofs / Christian Sternagel and René Thiemann -- A Compact Proof of Decidability for Regular Expression Equivalence / Andrea Asperti -- Using Locales to Define a Rely-Guarantee Temporal Logic / William Mansky and Elsa L. Gunter -- Charge! A Framework for Higher-Order Separation Logic in Coq / Jesper Bengtson, Jonas Braband Jensen and Lars Birkedal -- Mechanised Separation Algebra / Gerwin Klein, Rafal Kolanski and Andrew Boyton -- Directions in ISA Specification / Anthony Fox -- More SPASS with Isabelle: Superposition with Hard Sorts and Configurable Simplification / Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand and Christoph Weidenbach -- A Language of Patterns for Subterm Selection / Georges Gonthier and Enrico Tassi -- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL / Fabian Immler and Johannes Hölzl -- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem / Lars Noschinski -- Standalone Tactics Using OpenTheory / Ramana Kumar and Joe Hurd -- Functional Programs: Conversions between Deep and Shallow Embeddings / Magnus O. Myreen.
Bibliography Includes bibliographical references and author index.
Summary This book constitutes the thoroughly refereed proceedings of the Third International Conference on Interactive Theorem Proving, ITP 2012, held in Princeton, NJ, USA, in August 2012. The 21 revised full papers presented together with 4 rough diamond papers, 3 invited talks, and one invited tutorial were carefully reviewed and selected from 40 submissions. Among the topics covered are formalization of mathematics; program abstraction and logics; data structures and synthesis; security; (non- )termination and automata; program verification; theorem prover development; reasoning about program execution; and prover infrastructure and modeling styles.
Other author Beringer, Lennart.
Felty, Amy.
SpringerLink issuing body.
Subject Automatic theorem proving -- Congresses.
Software engineering -- Congresses.
Computer science.
Software engineering.
Data protection.
Logic design.
Artificial intelligence.
Mathematical Logic and Formal Languages.
Logics and Meanings of Programs.
Systems and Data Security.
Computation by Abstract Devices.
Electronic books.
Conference papers and proceedings.
Variant Title ITP 2012
ISBN 9783642323478