Skip to content

Conference on Interactive Theorem Proving (previously TPHOLs, changed in 2009)

ITP

B

CORE rank

CORE rank (raw)

B

Fields of research

Theory of Computation

Papers indexed

608

2010–2026

Papers per year

201065 peak2026

ITP papers

608 records sourced from DBLP. Search titles, filter by year, sort by recency.

YearTitleAuthors
2011ProofWiki.Matt Westwood
2011Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers.Matej Urbas, Mateja Jamnik
2011Content-based encoding of mathematical and code libraries.Josef Urban
2011Dynamic Proof Pages.Carst Tankink, James McKinna
2011The On-Line Encyclopedia of Integer Sequences: From Punched Cards to Wiki in 46 Years (abstract; invited talk).Neil J. A. Sloane
2011seL4 Enforces Integrity.Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
2011Composable Discovery Engines for Interactive Theorem Proving.Phil Scott, Jacques D. Fleuriot
2011Automatic Differentiation in ACL2.Peter Reid, Ruben Gamboa
2011Ideas for a MathWiki Editor.Sebastian Reichelt
2011Lem: A Lightweight Tool for Heavyweight Semantics.Scott Owens, Peter Bhm, Francesco Zappa Nardelli, Peter Sewell
2011Mechanised Computability Theory.Michael Norrish
2011Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism.Tobias Nipkow
2011A Verified Runtime for a Verified Theorem Prover.Magnus O. Myreen, Jared Davis
2011On the Generation of Positivstellensatz Witnesses in Degenerate Cases.David Monniaux, Pierre Corbineau
2011Formalization of Entropy Measures in HOL.Tarek Mhamdi, Osman Hasan, Sofine Tahar
2011Animating the Formalised Semantics of a Java-Like Language.Andreas Lochbihler, Lukas Bulwahn
2011Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials.Laureano Lambn, Francisco-Jess Martn-Mateos, Julio Rubio, Jos-Luis Ruiz-Reina
2011Wiki Authoring and Semantics of Mathematical Document Structure.Hiraku Kuroda, Takao Namiki
2011Proving Valid Quantified Boolean Formulas in HOL Light.Ondrej Kuncar
2011Validating QBF Validity in HOL4.Ramana Kumar, Tjark Weber
2011Termination of Isabelle Functions via Termination of Rewriting.Alexander Krauss, Christian Sternagel, Ren Thiemann, Carsten Fuhs, Jrgen Giesl
2011Challenges in Verifying Communication Fabrics.Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov
2011Logical Formalisation and Analysis of the Mifare Classic Card in PVS.Bart Jacobs, Ronny Wichers Schreur
2011Three Chapters of Measure Theory in Isabelle/HOL.Johannes Hlzl, Armin Heller
2011A Formalization of Polytime Functions.Sylvain Heraud, David Nowak
526550 of 608← PreviousNext →

Comparable venues

Other A*/A conferences filed under the same field of research.