Interactive Theorem Proving: First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings
Matt Kaufmann, Lawrence C. Paulson
Springer Science & Business Media, Jun 30, 2010 - Computers - 495 pages
This volume contains the papers presented at ITP 2010: the First International ConferenceonInteractiveTheoremProving. It washeldduring July11-14,2010 in Edinburgh, Scotland as part of the Federated Logic Conference (FLoC, July 9-21, 2010) alongside the other FLoC conferences and workshops. ITP combines the communities of two venerable meetings: the TPHOLs c- ference and the ACL2 workshop. The former conference originated in 1988 as a workshop for users of the HOL proof assistant. The ?rst two meetings were at the University of Cambridge, but afterwards they were held in a variety of venues. By 1992, the workshop acquired the name Higher-Order Logic Theorem Proving and Its Applications. In 1996, it was christened anew as Theorem Pr- ing in Higher-Order Logics, TPHOLs for short, and was henceforth organizedas a conference. Each of these transitions broadened the meeting's scope from the original HOL system to include other proof assistants based on forms of high- order logic, including Coq, Isabelle and PVS. TPHOLs has regularly published research done using ACL2 (the modern version of the well-known Boyer-Moore theorem prover), even though ACL2 implements a unique computational form of ?rst-order logic. The ACL2 community has run its own series of workshops since1999. BymergingTPHOLswith the ACL2workshop,weinclude a broader community of researchers who work with interactive proof tools. With our enlarged community, it was not surprising that ITP attracted a record-breaking 74 submissions, each of which was reviewed by at least three Programme Committee members.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
abstract abstract interpreter ACL2 algebra algorithm applied atoms automated automatically axiom Boolean certiﬁcates computation condition conﬁguration construct constructor context critical pair data structures datatype deﬁned deﬁnition diﬀerent eﬃcient encoding equal equations equivalent evaluation example ﬁnite ﬁrst ﬁrst-order ﬁxed point formal goal graph Heidelberg Heidelberg 2010 higher-order higher-order logic HOL Light HOL4 implementation inductive inﬁnite instantiation integral Isabelle Isabelle/HOL iteration Kleene algebra language LCF-style Lebesgue Lebesgue integral Lemma LNCS logic memoization natural numbers node OCaml operations optimal permutation powerlists predicate properties prove quantiﬁers relation result rewriting rules satisﬁes Section semantics sequentially consistent simpliﬁcation speciﬁcation Springer store buﬀer substitution subterm suﬃcient Switching Lemma tactic term termination theorem prover theory tion TPHOLs type classes type theory uniﬁcation variables veriﬁcation