| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Amelia Livingston |
Group Cohomology in the Lean Community Library.  |
ITP  |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominique Larchey-Wendling, Jean-François Monin |
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Dvorak, Jasmin Blanchette |
Closure Properties of General Grammars - Formally Verified. |
ITP |
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). |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | María Inés de Frutos-Fernández |
Formalizing Norm Extensions and Applications to Number Theory. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jujian Zhang |
Formalising the Proj Construction in Lean. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Angeliki Koutsoukou-Argyraki |
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001 |
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen |
Formalizing Functions as Processes. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Grabowski, Artur Kornilowicz |
Implementing More Explicit Definitional Expansions in Mizar (Short Paper). |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Yiming Xu, Michael Norrish |
Dependently Sorted Theorem Proving for Mathematical Foundations. |
ITP |
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. |
ITP |
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. |
ITP |
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. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Wojciech Nawrocki, Edward W. Ayers, Gabriel Ebner |
An Extensible User Interface for Lean 4. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Mario Carneiro |
Reimplementing Mizar in Rust. |
ITP |
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. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Guilloud, Sankalp Gambhir, Viktor Kuncak |
LISA - A Modern Proof System. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Oskar Abrahamsson, Magnus O. Myreen |
Fast, Verified Computation for Candle. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Chengsong Tan, Christian Urban |
POSIX Lexing with Bitcoded Derivatives. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Christina Kohl, Aart Middeldorp |
Formalizing Almost Development Closed Critical Pairs (Short Paper). |
ITP |
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 |
ITP |
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. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Niels van der Weide, Deivid Vale, Cynthia Kop |
Certifying Higher-Order Polynomial Interpretations. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone |
A Sound and Complete Projection for Global Types. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
A Proof-Producing Compiler for Blockchain Applications. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Luís Cruz-Filipe, Fabrizio Montesi |
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jarl G. Taxerås Flaten |
Formalising Yoneda Ext in Univalent Foundations. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Oliver Nash |
A Formalisation of Gallagher's Ergodic Theorem. |
ITP |
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. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Niels F. W. Voorneveld |
Slice Nondeterminism. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Philipp Joram, Niccolò Veltri |
Constructive Final Semantics of Finite Bags. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Mario Carneiro, Chad E. Brown, Josef Urban |
Automated Theorem Proving for Metamath. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Balázs Tóth, Tobias Nipkow |
Real-Time Double-Ended Queue Verified (Proof Pearl). |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Robbert Krebbers |
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohammad Abdulaziz, Christoph Madlener |
A Formal Analysis of RANKING. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Akihisa Yamada 0002, Jérémy Dubut |
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). |
ITP |
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. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence Dunn, Val Tannen, Steve Zdancewic |
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth |
Formalized functional analysis with semilinear maps. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Yury Kudryashov |
Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. |
ITP |
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. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Chelsea Edmonds, Lawrence C. Paulson |
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominik Kirst |
Computational Back-And-Forth Arguments in Constructive Type Theory. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell |
Candle: A Verified Implementation of HOL Light. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Arve Gengelbach, Johannes Åman Pohjola |
A Verified Cyclicity Checker: For Theories with Overloaded Constants. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty |
Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Malgorzata Biernacka, Witold Charatonik, Tomasz Drab |
The Zoo of Lambda-Calculus Reduction Strategies, And Coq. |
ITP |
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. |
ITP |
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. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Koundinya Vajjha, Barry M. Trager, Avraham Shinnar, Vasily Pestun |
Formalization of a Stochastic Approximation Theorem. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel |
Seventeen Provers Under the Hammer. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Anne Baanen |
Use and Abuse of Instance Parameters in the Lean Mathematical Library. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Hostert, Andrej Dudenhefner, Dominik Kirst |
Undecidability of Dyadic First-Order Logic in Coq. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Bohua Zhan |
User Interface Design in the HolPy Theorem Prover (Invited Talk). |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Kazuhiko Sakaguchi |
Reflexive Tactics for Algebra, Revisited. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich |
Refinement of Parallel Algorithms down to LLVM. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Karol Pak, Cezary Kaliszyk |
Formalizing a Diophantine Representation of the Set of Prime Numbers. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Emin Karayel |
Formalization of Randomized Approximation Algorithms for Frequency Moments. |
ITP |
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. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu |
Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. |
ITP |
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. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Jagadish Bapanapally, Ruben Gamboa |
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin |
Dandelion: Certified Approximations of Elementary Functions. |
ITP |
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. |
ITP |
2022 |
DBLP BibTeX RDF |
|
| 1 | Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas |
Mechanizing Soundness of Off-Policy Evaluation. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacob Prinz, G. A. Kavvos, Leonidas Lampropoulos |
Deeper Shallow Embeddings. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Yaël Dillies, Bhavik Mehta |
Formalising Szemerédi's Regularity Lemma in Lean. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
ITP |
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. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban |
The Isabelle ENIGMA. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Fabian Kunze, Nils Lauermann |
Synthetic Kolmogorov Complexity in Coq. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | María Inés de Frutos-Fernández |
Formalizing the Ring of Adèles of a Global Field. |
ITP |
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. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Konrad Slind |
Specifying Message Formats with Contiguity Types. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Floris van Doorn |
Formalized Haar Measure. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Lennard Gäher, Fabian Kunze |
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Brun 0002, Sára Decova, Andrea Lattuada, Dmitriy Traytel |
Verified Progress Tracking for Timely Dataflow. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Doczkal |
A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrei Popescu 0001, Thomas Bauereiss, Peter Lammich |
Bounded-Deducibility Security (Invited Paper). |
ITP |
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. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh |
Verified Double Sided Auctions for Financial Markets. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Seulkee Baek |
A Formally Verified Checker for First-Order Proofs. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub |
Unsolvability of the Quintic Formalized in Dependent Type Theory. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Marco Maggesi, Cosimo Perini Brogi |
A Formal Proof of Modal Completeness for Provability Logic. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Edward W. Ayers, Mateja Jamnik, William T. Gowers |
A Graphical User Interface Framework for Formal Verification. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller, David Fuenmayor |
Value-Oriented Legal Argumentation in Isabelle/HOL. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Laurent Théry |
Proof Pearl : Playing with the Tower of Hanoi Formally. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominik Kirst, Marc Hermes |
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Besson |
Itauto: An Extensible Intuitionistic SAT Solver. |
ITP |
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. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Nadia Polikarpova |
Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). |
ITP |
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. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Meven Lennon-Bertrand |
Complete Bidirectional Typing for the Calculus of Inductive Constructions. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Joshua Chen |
Homotopy Type Theory in Isabelle. |
ITP |
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). |
ITP |
2021 |
DBLP BibTeX RDF |
|
| 1 | Andreas Lochbihler |
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. |
ITP |
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. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license