Interactive Theorem Proving: Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings
Marko Van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk
Springer Science & Business Media, Aug 2, 2011 - Computers - 383 pages
This book constitutes the refereed proceedings of the Second International Conference on Interactive Theorem proving, ITP 2011, held in Berg en Dal, The Netherlands, in August 2011.
The 25 revised full papers presented were carefully reviewed and selected from 50 submissions. Among the topics covered are counterexample generation, verification, validation, term rewriting, theorem proving, computability theory, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
abstract ACL2 algebra algorithm apply automatically automation Bellantoni-Cook’s class bool Boolean bytecode certificate chain compiler Computer defderivative deﬁne defined definition derivative encoding equation equivalence classes evaluation example execution extended reals extension variables finite formal formalisation formula graphs Heidelberg higher-order higher-order logic HOL Light HOL4 implementation induction instantiate interface interpretation Isabelle Isabelle/HOL JinjaThreads Jitawa kernel keystream language LCF-style Lebesgue integral Lebesgue measure Lemma LFSR linear Linear Logic LNCS logic maps matrix measure spaces Mifare Milawa narrative natural numbers Nikodym OCaml operations parameter polynomial predicate problem proof assistant properties prove quantifiers real numbers recursive functions regular expression relation result rewrite rules seL4 semantics sequence simplicial polynomials simplicial set simulation solvers specification Springer Squolem structure term termination theorem prover theory tion tool TPHOLs unary valid variables vector verified