default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID10th ITP 2019: Portland, OR, USA
- John Harrison, John O'Leary, Andrew Tolmach:
10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA. LIPIcs 141, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2019, ISBN 978-3-95977-122-1 - Front Matter, Table of Contents, Preface, Conference Organization. 0:1-0:14
- June Andronick:
A Million Lines of Proof About a Moving Target (Invited Talk). 1:1-1:1 - Kevin Buzzard:
What Makes a Mathematician Tick? (Invited Talk). 2:1-2:1 - Martin Dixon:
An Increasing Need for Formality (Invited Talk). 3:1-3:1 - Mohammad Abdulaziz
, Charles Gretton, Michael Norrish:
A Verified Compositional Algorithm for AI Planning. 4:1-4:19 - Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka:
Proving Tree Algorithms for Succinct Data Structures. 5:1-5:19 - Jeremy Avigad, Mario Carneiro, Simon Hudon:
Data Types as Quotients of Polynomial Functors. 6:1-6:19 - Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux:
Primitive Floats in Coq. 7:1-7:20 - Florent Bréhard, Assia Mahboubi, Damien Pous:
A Certificate-Based Approach to Formally Verified Approximations. 8:1-8:19 - Chad E. Brown, Cezary Kaliszyk, Karol Pak:
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. 9:1-9:16 - Matthias Brun, Dmitriy Traytel:
Generic Authenticated Data Structures, Formally. 10:1-10:18 - Julian Brunner, Benedikt Seidl, Salomon Sickert:
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. 11:1-11:19 - Mario Carneiro:
Formalizing Computability Theory via Partial Recursive Functions. 12:1-12:17 - Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry:
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. 13:1-13:19 - Lukasz Czajka:
First-Order Guarded Coinduction in Coq. 14:1-14:18 - Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis:
Formalizing the Solution to the Cap Set Problem. 15:1-15:19 - Manuel Eberl:
Nine Chapters of Analytic Number Theory in Isabelle/HOL. 16:1-16:19 - Yannick Forster, Fabian Kunze:
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. 17:1-17:19 - Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier:
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. 18:1-18:20 - Jesse Michael Han, Floris van Doorn:
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. 19:1-19:19 - Maximilian P. L. Haslbeck, Peter Lammich:
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. 20:1-20:18 - Fabian Immler, Jonas Rädle, Makarius Wenzel:
Virtualization of HOL4 in Isabelle. 21:1-21:18 - Peter Lammich:
Generating Verified LLVM from Isabelle/HOL. 22:1-22:19 - Peter Lammich, Tobias Nipkow:
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. 23:1-23:18 - Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux:
A Verified LL(1) Parser Generator. 24:1-24:18 - Mihir Parang Mehta, William R. Cook:
Binary-Compatible Verification of Filesystems with ACL2. 25:1-25:18 - Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman:
Ornaments for Proof Reuse in Coq. 26:1-26:19 - Robert Sison, Toby Murray:
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. 27:1-27:19 - Florian Steinberg, Laurent Théry, Holger Thies:
Quantitative Continuity and Computable Analysis in Coq. 28:1-28:21 - Enrico Tassi:
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. 29:1-29:18 - Akihisa Yamada, Jérémy Dubut:
Complete Non-Orders and Fixed Points. 30:1-30:16 - Minchao Wu, Rajeev Goré:
Verified Decision Procedures for Modal Logics. 31:1-31:19 - Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen:
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. 32:1-32:19 - Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher:
The DPRM Theorem in Isabelle (Short Paper). 33:1-33:7 - Jan Jakubuv, Josef Urban:
Hammering Mizar by Learning Clause Guidance (Short Paper). 34:1-34:8 - Cezary Kaliszyk, Karol Pak:
Declarative Proof Translation (Short Paper). 35:1-35:7 - Daniel E. Severín:
Formalization of the Domination Chain with Weighted Parameters (Short Paper). 36:1-36:7
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 2024-12-19 22:21 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:
