ITP is an international conference on Interactive Theorem Proving and related issues including applications, case studies, foundations, languages, and implementations. It is a combination of TPHOLs (Theorem Proving in Higher Order Logics) and the ACL2 Workshop series. ITP 2010 is the 23rd meeting in the TPHOLs series and the 9th meeting in the ACL2 Workshop series.
Springer in the LNCS series.
- Gerwin Klein
A Formally Verified OS Kernel. Now What?
- Benjamin Pierce
Proof Assistant as Teaching Assistant: A View from the Trenches