Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. ProceedingsThis 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. |
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
Interactive Theorem Proving: Third International Conference, ITP 2012 ... Lennart Beringer,Amy Felty No preview available - 2012 |
Common terms and phrases
abstract interpreter ACL2 algebraic numbers algorithm applied argument assertion assumptions automated automatically bound Cauchy reals Cauchy sequence Computer construction context cprec datatype decision procedure define definition differential equations differential invariants domain element embedding encoding equivalence Euler method example finite formalisation formalization goal graph Heidelberg Heidelberg 2012 implementation induction instantiate Isabelle Isabelle/HOL language Lemma LNCS loop matching method MetiTarski monad multiset notation operations pattern polynomial precondition predicate Priority Inversion probabilistic problem proof assistant properties prove real closed field real numbers recursive redex refinement regular expression relation result rewrite RGTL rule Section semantics separation logic sequence setoid simplify-mp solution SPASS Springer SSReflect step strategy structure subterms tactics term termination theorem prover thread TPHOLs type theory update variables verified
Bibliographic information
| Title | Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings Volume 7406 of Lecture Notes in Computer Science Theoretical Computer Science and General Issues |
| Editors | Lennart Beringer, Amy Felty |
| Edition | illustrated |
| Publisher | Springer, 2012 |
| ISBN | 3642323472, 9783642323478 |
| Length | 419 pages |
| Subjects | › › Computers / Artificial Intelligence / General Computers / Computer Science Computers / Information Technology Computers / Machine Theory Computers / Programming / General Computers / Security / General Computers / Software Development & Engineering / General Mathematics / Discrete Mathematics Mathematics / Logic |
| Export Citation | BiBTeX EndNote RefMan |