Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Amelia Livingston |
Group Cohomology in the Lean Community Library. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 22:1-22:17, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Larchey-Wendling, Jean-François Monin |
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 21:1-21:17, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 0:1-0:10, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Martin Dvorak, Jasmin Blanchette |
Closure Properties of General Grammars - Formally Verified. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 15:1-15:16, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi |
Fermat's Last Theorem for Regular Primes (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 36:1-36:8, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | María Inés de Frutos-Fernández |
Formalizing Norm Extensions and Applications to Number Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 13:1-13:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Jujian Zhang |
Formalising the Proj Construction in Lean. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 35:1-35:17, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Angeliki Koutsoukou-Argyraki |
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 1:1-1:2, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001 |
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 18:1-18:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen |
Formalizing Functions as Processes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 5:1-5:21, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Adam Grabowski, Artur Kornilowicz |
Implementing More Explicit Definitional Expansions in Mizar (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 37:1-37:8, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Yiming Xu, Michael Norrish |
Dependently Sorted Theorem Proving for Mathematical Foundations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 33:1-33:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, Talia Ringer |
Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 26:1-26:20, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | David Kurniadi Angdinata, Junyan Xu |
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 6:1-6:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann |
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 12:1-12:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Wojciech Nawrocki, Edward W. Ayers, Gabriel Ebner |
An Extensible User Interface for Lean 4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 24:1-24:20, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Mario Carneiro |
Reimplementing Mizar in Rust. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 10:1-10:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel |
Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 25:1-25:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Simon Guilloud, Sankalp Gambhir, Viktor Kuncak |
LISA - A Modern Proof System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 17:1-17:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Oskar Abrahamsson, Magnus O. Myreen |
Fast, Verified Computation for Candle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 4:1-4:17, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Chengsong Tan, Christian Urban |
POSIX Lexing with Bitcoded Derivatives. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 27:1-27:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Christina Kohl, Aart Middeldorp |
Formalizing Almost Development Closed Critical Pairs (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 38:1-38:8, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Adam Naumowicz, René Thiemann (eds.) |
14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6 The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
1 | Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz 0001, Martin Suda 0001, Josef Urban |
MizAR 60 for Mizar 50. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 19:1-19:22, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Niels van der Weide, Deivid Vale, Cynthia Kop |
Certifying Higher-Order Polynomial Interpretations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 30:1-30:20, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone |
A Sound and Complete Projection for Global Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 28:1-28:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
A Proof-Producing Compiler for Blockchain Applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 7:1-7:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Luís Cruz-Filipe, Fabrizio Montesi |
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 11:1-11:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Jarl G. Taxerås Flaten |
Formalising Yoneda Ext in Univalent Foundations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 16:1-16:17, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Oliver Nash |
A Formalisation of Gallagher's Ergodic Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 23:1-23:16, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel |
Foundational Verification of Stateful P4 Packet Processing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 32:1-32:20, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Niels F. W. Voorneveld |
Slice Nondeterminism. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 31:1-31:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Philipp Joram, Niccolò Veltri |
Constructive Final Semantics of Finite Bags. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 20:1-20:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Mario Carneiro, Chad E. Brown, Josef Urban |
Automated Theorem Proving for Metamath. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 9:1-9:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Balázs Tóth, Tobias Nipkow |
Real-Time Double-Ended Queue Verified (Proof Pearl). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 29:1-29:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Robbert Krebbers |
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 2:1-2:1, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Mohammad Abdulaziz, Christoph Madlener |
A Formal Analysis of RANKING. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 3:1-3:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Akihisa Yamada 0002, Jérémy Dubut |
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 34:1-34:13, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Roger Bosman, Georgios Karachalias, Tom Schrijvers |
No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 8:1-8:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Lawrence Dunn, Val Tannen, Steve Zdancewic |
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 14:1-14:20, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
1 | Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth |
Formalized functional analysis with semilinear maps. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 10:1-10:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Yury Kudryashov |
Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 23:1-23:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Nicolas Magaud |
Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 25:1-25:17, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Chelsea Edmonds, Lawrence C. Paulson |
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 11:1-11:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Dominik Kirst |
Computational Back-And-Forth Arguments in Constructive Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 22:1-22:12, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell |
Candle: A Verified Implementation of HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 3:1-3:17, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Arve Gengelbach, Johannes Åman Pohjola |
A Verified Cyclicity Checker: For Theories with Overloaded Constants. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 15:1-15:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty |
Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 1:1-1:2, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Malgorzata Biernacka, Witold Charatonik, Tomasz Drab |
The Zoo of Lambda-Calculus Reduction Strategies, And Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 7:1-7:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen |
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 20:1-20:22, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Asta Halkjær From, Frederik Krogsdal Jacobsen |
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 13:1-13:22, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Koundinya Vajjha, Barry M. Trager, Avraham Shinnar, Vasily Pestun |
Formalization of a Stochastic Approximation Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 31:1-31:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel |
Seventeen Provers Under the Hammer. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 8:1-8:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Anne Baanen |
Use and Abuse of Instance Parameters in the Lean Mathematical Library. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 4:1-4:20, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Johannes Hostert, Andrej Dudenhefner, Dominik Kirst |
Undecidability of Dyadic First-Order Logic in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 19:1-19:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Bohua Zhan |
User Interface Design in the HolPy Theorem Prover (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 2:1-2:1, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Kazuhiko Sakaguchi |
Reflexive Tactics for Algebra, Revisited. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 29:1-29:22, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Peter Lammich |
Refinement of Parallel Algorithms down to LLVM. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 24:1-24:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Karol Pak, Cezary Kaliszyk |
Formalizing a Diophantine Representation of the Set of Prime Numbers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 26:1-26:8, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Emin Karayel |
Formalization of Randomized Approximation Algorithms for Frequency Moments. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 21:1-21:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia |
Compositional Verification of Interacting Systems Using Event Monads. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 33:1-33:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu |
Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 30:1-30:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala |
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 18:1-18:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Jagadish Bapanapally, Ruben Gamboa |
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 5:1-5:15, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin |
Dandelion: Certified Approximations of Elementary Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 6:1-6:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | June Andronick, Leonardo de Moura 0001 (eds.) |
13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5 The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
1 | Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas |
Mechanizing Soundness of Off-Policy Evaluation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 32:1-32:20, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Jacob Prinz, G. A. Kavvos, Leonidas Lampropoulos |
Deeper Shallow Embeddings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 28:1-28:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Yaël Dillies, Bhavik Mehta |
Formalising Szemerédi's Regularity Lemma in Lean. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 9:1-9:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 0:1-0:10, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, Michael Norrish |
Kalas: A Verified, End-To-End Compiler for a Choreographic Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 27:1-27:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban |
The Isabelle ENIGMA. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 16:1-16:21, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Yannick Forster 0002, Fabian Kunze, Nils Lauermann |
Synthetic Kolmogorov Complexity in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 12:1-12:19, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | María Inés de Frutos-Fernández |
Formalizing the Ring of Adèles of a Global Field. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 14:1-14:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala |
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 17:1-17:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
1 | Konrad Slind |
Specifying Message Formats with Contiguity Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 30:1-30:17, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Floris van Doorn |
Formalized Haar Measure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 18:1-18:17, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Lennard Gäher, Fabian Kunze |
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 20:1-20:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Brun 0002, Sára Decova, Andrea Lattuada, Dmitriy Traytel |
Verified Progress Tracking for Timely Dataflow. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 10:1-10:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Christian Doczkal |
A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 17:1-17:17, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Andrei Popescu 0001, Thomas Bauereiss, Peter Lammich |
Bounded-Deducibility Security (Invited Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 3:1-3:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio |
A Formalization of Dedekind Domains and Class Groups of Global Fields. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 5:1-5:19, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh |
Verified Double Sided Auctions for Financial Markets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 28:1-28:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Seulkee Baek |
A Formally Verified Checker for First-Order Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 6:1-6:13, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 0:1-0:8, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub |
Unsolvability of the Quintic Formalized in Dependent Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 8:1-8:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Marco Maggesi, Cosimo Perini Brogi |
A Formal Proof of Modal Completeness for Provability Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 26:1-26:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Edward W. Ayers, Mateja Jamnik, William T. Gowers |
A Graphical User Interface Framework for Formal Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 4:1-4:16, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Benzmüller, David Fuenmayor |
Value-Oriented Legal Argumentation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 7:1-7:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Laurent Théry |
Proof Pearl : Playing with the Tower of Hanoi Formally. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 31:1-31:16, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Dominik Kirst, Marc Hermes |
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 23:1-23:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Frédéric Besson |
Itauto: An Extensible Intuitionistic SAT Solver. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 9:1-9:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li 0004, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic |
Verifying an HTTP Key-Value Server with Interaction Trees and VST. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 32:1-32:19, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Nadia Polikarpova |
Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 2:1-2:1, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Yannick Forster 0002, Fabian Kunze, Gert Smolka, Maxi Wuttke |
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 19:1-19:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Meven Lennon-Bertrand |
Complete Bidirectional Typing for the Calculus of Inductive Constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 24:1-24:19, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Joshua Chen |
Homotopy Type Theory in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 12:1-12:8, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Liron Cohen 0001, Cezary Kaliszyk (eds.) |
12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7 The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
1 | Andreas Lochbihler |
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 25:1-25:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Katherine Cordwell, Yong Kiam Tan, André Platzer |
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 14:1-14:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|