| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti |
Formalising a Turing-Complete Choreographic Language in Coq.  |
ITP  |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Adrian De Lon, Peter Koepke, Anton Lorenzen |
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Nigron, Pierre-Évariste Dagand |
Reaching for the Star: Tale of a Monad in Coq. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Stepan Holub, Stepán Starosta |
Formalization of Basic Combinatorics on Words. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Kesha Hietala, Robert Rand 0001, Shih-Han Hung, Liyi Li 0002, Michael Hicks 0001 |
Proving Quantum Programs Correct. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz |
Syntactic-Semantic Form of Mizar Articles. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Luca Ciccone, Francesco Dagnino, Elena Zucca |
Flexible Coinduction in Agda. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, Thiago Mendonça Ferreira Ramos |
Formal Verification of Termination Criteria for First-Order Recursive Functions. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Magnus O. Myreen |
The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Brun 0002, Dmitriy Traytel |
Generic Authenticated Data Structures, Formally. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | John Harrison 0001, John O'Leary, Andrew Tolmach (eds.) |
10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA. |
ITP |
2019 |
DBLP BibTeX RDF |
|
| 1 | Chad E. Brown, Cezary Kaliszyk, Karol Pak |
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher |
The DPRM Theorem in Isabelle (Short Paper). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich, Tobias Nipkow |
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen |
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka |
Proving Tree Algorithms for Succinct Data Structures. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis |
Formalizing the Solution to the Cap Set Problem. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Dixon |
An Increasing Need for Formality (Invited Talk). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Sison, Toby Murray |
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux |
A Verified LL(1) Parser Generator. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Akihisa Yamada 0002, Jérémy Dubut |
Complete Non-Orders and Fixed Points. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux |
Primitive Floats in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Jakubuv, Josef Urban |
Hammering Mizar by Learning Clause Guidance (Short Paper). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Kevin Buzzard |
What Makes a Mathematician Tick? (Invited Talk). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Enrico Tassi |
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohammad Abdulaziz, Charles Gretton, Michael Norrish |
A Verified Compositional Algorithm for AI Planning. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesse Michael Han, Floris van Doorn |
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
Ornaments for Proof Reuse in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich |
Generating Verified LLVM from Isabelle/HOL. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Julian Brunner 0001, Benedikt Seidl, Salomon Sickert |
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Karol Pak |
Declarative Proof Translation (Short Paper). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Mihir Parang Mehta, William R. Cook |
Binary-Compatible Verification of Filesystems with ACL2. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Steinberg 0001, Laurent Théry, Holger Thies |
Quantitative Continuity and Computable Analysis in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy Avigad, Mario Carneiro, Simon Hudon |
Data Types as Quotients of Polynomial Functors. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Florent Bréhard, Assia Mahboubi, Damien Pous |
A Certificate-Based Approach to Formally Verified Approximations. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Lukasz Czajka 0001 |
First-Order Guarded Coinduction in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Mario Carneiro |
Formalizing Computability Theory via Partial Recursive Functions. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Manuel Eberl |
Nine Chapters of Analytic Number Theory in Isabelle/HOL. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Minchao Wu, Rajeev Goré |
Verified Decision Procedures for Modal Logics. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Fabian Kunze |
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel E. Severín |
Formalization of the Domination Chain with Weighted Parameters (Short Paper). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Maximilian P. L. Haslbeck, Peter Lammich |
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | June Andronick |
A Million Lines of Proof About a Moving Target (Invited Talk). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabian Immler, Jonas Rädle, Makarius Wenzel |
Virtualization of HOL4 in Isabelle. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier |
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Hira Taqdees Syeda, Gerwin Klein |
Program Verification in the Presence of Cached Address Translation. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Callum Bannister, Peter Höfner, Gerwin Klein |
Backwards and Forwards with Separation Logic. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel |
A Formally Verified Solver for Homogeneous Linear Diophantine Equations. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer |
Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú |
Boosting the Reuse of Formal Specifications. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers |
Formalization of a Polymorphic Subtyping Algorithm. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Manuel Eberl, Max W. Haslbeck, Tobias Nipkow |
Verified Analysis of Random Binary Tree Structures. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Raphaël Cauderlier |
Tactics and Certificates in Meta Dedukti. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe |
Physical Addressing on Real Hardware in Isabelle/HOL. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen |
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy Avigad, Assia Mahboubi |
Erratum to: Interactive Theorem Proving. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Colm Baston, Venanzio Capretta |
The Coinductive Formulation of Common Knowledge. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau |
Towards Certified Meta-Programming with Typed Template-Coq. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Wimmer 0001, Johannes Hölzl |
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler |
Fast Machine Words in Isabelle/HOL. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Ran Zmigrod, Matthew L. Daggitt, Timothy G. Griffin |
An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point Theory. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy Avigad, Assia Mahboubi (eds.) |
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 |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002 |
A Formalization of the LLL Basis Reduction Algorithm. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Julian Parsert, Cezary Kaliszyk |
Towards Formal Foundations for Game Theory. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette, William M. Farmer, Patrick Laskowski |
HOL Light QE. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Denis Firsov, Richard Blair, Aaron Stump |
Efficient Mendler-Style Lambda-Encodings in Cedille. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Andréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino |
Formalizing Ring Theory in PVS. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | João Paulo Pizani Flor, Wouter Swierstra |
Verified Timing Transformations in Synchronous Circuits with \lambda \pi -Ware. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandra Mendes, João F. Ferreira 0001 |
Towards Verified Handwritten Calculational Proofs - (Short Paper). |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvain Boulmé, Alexandre Maréchal |
A Coq Tactic for Equality Learning in Linear Arithmetic. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Edith Heiter, Gert Smolka |
Verification of PCP-Related Computational Reductions in Coq. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Doczkal, Guillaume Combette, Damien Pous |
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Wimmer 0001, Shuwei Hu, Tobias Nipkow |
Verified Memoization and Dynamic Programming. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic |
A Formal Equational Theory for Call-By-Push-Value. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfram Kahl |
CalcCheck: A Proof Checker for Teaching the "Logical Approach to Discrete Math". |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Étienne Miquey |
Formalizing Implicative Algebras in Coq. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler, Joshua Schneider 0001 |
Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominique Larchey-Wendling |
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph Tassarotti, Robert Harper 0001 |
Verified Tail Bounds for Randomized Programs. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Jantsch, Michael Norrish |
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins |
A Coq Formalisation of SQL's Execution Engines. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Samuel Balco, Sabine Frittella, Giuseppe Greco 0001, Alexander Kurz 0001, Alessandra Palmigiano |
Software Tool Support for Modular Reasoning in Modal Logics of Actions. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Jason Gross, Andres Erbsen, Adam Chlipala |
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz 0001, Josef Urban |
ProofWatch: Watchlist Guidance for Large Theories in E. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Bohua Zhan |
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava |
Certifying Standard and Stratified Datalog Inference Engines in SSReflect. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominik Kirst, Gert Smolka |
Categoricity Results for Second-Order ZF in Dependent Type Theory. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Gert Smolka |
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola |
A Verified Generational Garbage Collector for CakeML. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler |
Efficient, Verified Checking of Propositional Proofs. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Josef Urban, Jirí Vyskocil |
Automating Formalization by Statistical and Semantic Parsing of Mathematics. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominique Larchey-Wendling |
Typing Total Recursive Functions in Coq. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Cyril Cohen, Damien Rouhling |
A Formal Proof in Coq of LaSalle's Invariance Principle. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Julian Rosemann, Sigurd Schneider, Sebastian Hack |
Verified Spilling and Translation Validation with Repair. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler |
Effect Polymorphism in Higher-Order Logic (Proof Pearl). |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Raphaël Cauderlier, Catherine Dubois |
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Sophie Bernard |
Formalization of the Lindemann-Weierstrass Theorem. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Allamigeon, Ricardo D. Katz |
A Formalization of Convex Polyhedra Based on the Simplex Method. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license