TY - BOOK ID - 79535035 TI - Interactive Theorem Proving : First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings AU - Kaufmann, Matt AU - Paulson, Lawrence C AU - SpringerLink (Online service) PY - 2010 SN - 9783642140525 9783642140518 9783642140532 9783642142024 9783642142949 9783642141850 9783642137532 PB - Berlin Heidelberg Springer Berlin Heidelberg DB - UniCat KW - Mathematical logic KW - Logic KW - Immunology. Immunopathology KW - Computer science KW - Programming KW - Artificial intelligence. Robotics. Simulation. Graphics KW - Computer. Automation KW - monoklonale antilichamen KW - polyklonale antilichamen KW - immunologie KW - computers KW - programmeren (informatica) KW - programmeertalen KW - wiskunde KW - software engineering KW - KI (kunstmatige intelligentie) KW - logica KW - 681.3*B6 KW - 681.3*B6 Logic design (Hardware) KW - Logic design (Hardware) UR - https://www.unicat.be/uniCat?func=search&query=sysid:79535035 AB - 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. ER -