default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID9th ITP 2018: Oxford, UK
- Jeremy Avigad, Assia Mahboubi:
Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. Lecture Notes in Computer Science 10895, Springer 2018, ISBN 978-3-319-94820-1 - Reto Achermann, Lukas Humbel
, David A. Cock, Timothy Roscoe:
Physical Addressing on Real Hardware in Isabelle/HOL. 1-19 - Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau:
Towards Certified Meta-Programming with Typed Template-Coq. 20-39 - Andréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino:
Formalizing Ring Theory in PVS. 40-47 - Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano:
Software Tool Support for Modular Reasoning in Modal Logics of Actions. 48-67 - Callum Bannister, Peter Höfner, Gerwin Klein:
Backwards and Forwards with Separation Logic. 68-87 - Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins:
A Coq Formalisation of SQL's Execution Engines. 88-107 - Sylvain Boulmé, Alexandre Maréchal:
A Coq Tactic for Equality Learning in Linear Arithmetic. 108-125 - Colm Baston, Venanzio Capretta:
The Coinductive Formulation of Common Knowledge. 126-141 - Raphaël Cauderlier:
Tactics and Certificates in Meta Dedukti. 142-159 - Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Formalization of the LLL Basis Reduction Algorithm. 160-177 - Christian Doczkal, Guillaume Combette, Damien Pous:
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. 178-195 - Manuel Eberl, Max W. Haslbeck, Tobias Nipkow:
Verified Analysis of Random Binary Tree Structures. 196-214 - Jacques Carette, William M. Farmer, Patrick Laskowski:
HOL Light QE. 215-234 - Denis Firsov, Richard Blair, Aaron Stump:
Efficient Mendler-Style Lambda-Encodings in Cedille. 235-252 - Yannick Forster, Edith Heiter, Gert Smolka:
Verification of PCP-Related Computational Reductions in Coq. 253-269 - Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban:
ProofWatch: Watchlist Guidance for Large Theories in E. 270-288 - Jason Gross, Andres Erbsen, Adam Chlipala:
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. 289-305 - Simon Jantsch, Michael Norrish:
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. 306-323 - Wolfram Kahl:
CalcCheck: A Proof Checker for Teaching the "Logical Approach to Discrete Math". 324-341 - Alexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer:
Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY. 342-361 - Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen:
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). 362-369 - Dominique Larchey-Wendling:
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. 370-387 - Andreas Lochbihler:
Fast Machine Words in Isabelle/HOL. 388-410 - Andreas Lochbihler, Joshua Schneider:
Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. 411-431 - Alexandra Mendes, João F. Ferreira:
Towards Verified Handwritten Calculational Proofs - (Short Paper). 432-440 - Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel:
A Formally Verified Solver for Homogeneous Linear Diophantine Equations. 441-458 - Étienne Miquey:
Formalizing Implicative Algebras in Coq. 459-476 - Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú:
Boosting the Reuse of Formal Specifications. 477-494 - Julian Parsert, Cezary Kaliszyk:
Towards Formal Foundations for Game Theory. 495-503 - João Paulo Pizani Flor, Wouter Swierstra:
Verified Timing Transformations in Synchronous Circuits with \lambda \pi -Ware. 504-522 - Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic:
A Formal Equational Theory for Call-By-Push-Value. 523-541 - Hira Taqdees Syeda, Gerwin Klein:
Program Verification in the Presence of Cached Address Translation. 542-559 - Joseph Tassarotti, Robert Harper:
Verified Tail Bounds for Randomized Programs. 560-578 - Simon Wimmer, Shuwei Hu, Tobias Nipkow:
Verified Memoization and Dynamic Programming. 579-596 - Simon Wimmer, Johannes Hölzl:
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). 597-603 - Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers:
Formalization of a Polymorphic Subtyping Algorithm. 604-622 - Ran Zmigrod, Matthew L. Daggitt, Timothy G. Griffin:
An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point Theory. 623-639 - Jeremy Avigad, Assia Mahboubi:
Erratum to: Interactive Theorem Proving.
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-12-12 22:52 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
