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. ![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. 15:1-15: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 | Adrian De Lon, Peter Koepke, Anton Lorenzen |
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. ![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. 16:1-16:11, 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 | Pierre Nigron, Pierre-Évariste Dagand |
Reaching for the Star: Tale of a Monad 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. 29:1-29: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 | Stepan Holub, Stepán Starosta |
Formalization of Basic Combinatorics on Words. ![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. 22:1-22: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 | Kesha Hietala, Robert Rand 0001, Shih-Han Hung, Liyi Li 0002, Michael Hicks 0001 |
Proving Quantum Programs Correct. ![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. 21:1-21: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 | Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz |
Syntactic-Semantic Form of Mizar Articles. ![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. 11:1-11: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 | Luca Ciccone, Francesco Dagnino, Elena Zucca |
Flexible Coinduction in Agda. ![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. 13:1-13: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 | 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. ![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. 27:1-27: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 | Magnus O. Myreen |
The CakeML Project's Quest for Ever Stronger Correctness Theorems (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. 1:1-1:10, 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, Dmitriy Traytel |
Generic Authenticated Data Structures, Formally. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 10:1-10:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1 The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
1 | Chad E. Brown, Cezary Kaliszyk, Karol Pak |
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 9:1-9:16, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher |
The DPRM Theorem in Isabelle (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 33:1-33:7, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 23:1-23:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen |
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 32:1-32:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka |
Proving Tree Algorithms for Succinct Data Structures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 5:1-5:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis |
Formalizing the Solution to the Cap Set Problem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 15:1-15:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Martin Dixon |
An Increasing Need for Formality (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 3:1-3:1, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Robert Sison, Toby Murray |
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 27:1-27:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux |
A Verified LL(1) Parser Generator. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 24:1-24:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Akihisa Yamada 0002, Jérémy Dubut |
Complete Non-Orders and Fixed Points. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 30:1-30:16, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux |
Primitive Floats in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 7:1-7:20, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Jan Jakubuv, Josef Urban |
Hammering Mizar by Learning Clause Guidance (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 34:1-34:8, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Kevin Buzzard |
What Makes a Mathematician Tick? (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 2:1-2:1, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Enrico Tassi |
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 29:1-29:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Mohammad Abdulaziz, Charles Gretton, Michael Norrish |
A Verified Compositional Algorithm for AI Planning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 4:1-4:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | |
Front Matter, Table of Contents, Preface, Conference Organization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 0:1-0:14, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Jesse Michael Han, Floris van Doorn |
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 19:1-19:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
Ornaments for Proof Reuse in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 26:1-26:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Peter Lammich |
Generating Verified LLVM from Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 22:1-22:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Julian Brunner 0001, Benedikt Seidl, Salomon Sickert |
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 11:1-11:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Cezary Kaliszyk, Karol Pak |
Declarative Proof Translation (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 35:1-35:7, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Mihir Parang Mehta, William R. Cook |
Binary-Compatible Verification of Filesystems with ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 25:1-25:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Florian Steinberg 0001, Laurent Théry, Holger Thies |
Quantitative Continuity and Computable Analysis in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 28:1-28:21, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Jeremy Avigad, Mario Carneiro, Simon Hudon |
Data Types as Quotients of Polynomial Functors. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 6:1-6:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Florent Bréhard, Assia Mahboubi, Damien Pous |
A Certificate-Based Approach to Formally Verified Approximations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 8:1-8:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 13:1-13:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Lukasz Czajka 0001 |
First-Order Guarded Coinduction in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 14:1-14:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Mario Carneiro |
Formalizing Computability Theory via Partial Recursive Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 12:1-12:17, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Manuel Eberl |
Nine Chapters of Analytic Number Theory in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 16:1-16:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Minchao Wu, Rajeev Goré |
Verified Decision Procedures for Modal Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 31:1-31:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 17:1-17:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Daniel E. Severín |
Formalization of the Domination Chain with Weighted Parameters (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 36:1-36:7, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Maximilian P. L. Haslbeck, Peter Lammich |
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 20:1-20:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | June Andronick |
A Million Lines of Proof About a Moving Target (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 1:1-1:1, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Fabian Immler, Jonas Rädle, Makarius Wenzel |
Virtualization of HOL4 in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 21:1-21:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 18:1-18:20, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
1 | Hira Taqdees Syeda, Gerwin Klein |
Program Verification in the Presence of Cached Address Translation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 542-559, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Callum Bannister, Peter Höfner, Gerwin Klein |
Backwards and Forwards with Separation Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 68-87, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 441-458, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 342-361, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 477-494, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers |
Formalization of a Polymorphic Subtyping Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 604-622, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Manuel Eberl, Max W. Haslbeck, Tobias Nipkow |
Verified Analysis of Random Binary Tree Structures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 196-214, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Raphaël Cauderlier |
Tactics and Certificates in Meta Dedukti. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 142-159, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe |
Physical Addressing on Real Hardware in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 1-19, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 362-369, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Jeremy Avigad, Assia Mahboubi |
Erratum to: Interactive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Colm Baston, Venanzio Capretta |
The Coinductive Formulation of Common Knowledge. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 126-141, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau |
Towards Certified Meta-Programming with Typed Template-Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 20-39, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Simon Wimmer 0001, Johannes Hölzl |
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 597-603, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Lochbihler |
Fast Machine Words in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 388-410, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 623-639, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![Springer, 978-3-319-94820-1 The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 160-177, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Julian Parsert, Cezary Kaliszyk |
Towards Formal Foundations for Game Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 495-503, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Jacques Carette, William M. Farmer, Patrick Laskowski |
HOL Light QE. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 215-234, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Denis Firsov, Richard Blair, Aaron Stump |
Efficient Mendler-Style Lambda-Encodings in Cedille. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 235-252, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Andréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino |
Formalizing Ring Theory in PVS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 40-47, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | João Paulo Pizani Flor, Wouter Swierstra |
Verified Timing Transformations in Synchronous Circuits with \lambda \pi -Ware. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 504-522, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Alexandra Mendes, João F. Ferreira 0001 |
Towards Verified Handwritten Calculational Proofs - (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 432-440, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Sylvain Boulmé, Alexandre Maréchal |
A Coq Tactic for Equality Learning in Linear Arithmetic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 108-125, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Yannick Forster 0002, Edith Heiter, Gert Smolka |
Verification of PCP-Related Computational Reductions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 253-269, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Christian Doczkal, Guillaume Combette, Damien Pous |
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 178-195, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Simon Wimmer 0001, Shuwei Hu, Tobias Nipkow |
Verified Memoization and Dynamic Programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 579-596, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic |
A Formal Equational Theory for Call-By-Push-Value. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 523-541, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Wolfram Kahl |
CalcCheck: A Proof Checker for Teaching the "Logical Approach to Discrete Math". ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 324-341, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Étienne Miquey |
Formalizing Implicative Algebras in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 459-476, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Lochbihler, Joshua Schneider 0001 |
Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 411-431, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Larchey-Wendling |
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 370-387, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Joseph Tassarotti, Robert Harper 0001 |
Verified Tail Bounds for Randomized Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 560-578, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Simon Jantsch, Michael Norrish |
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 306-323, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins |
A Coq Formalisation of SQL's Execution Engines. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 88-107, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 48-67, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 289-305, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz 0001, Josef Urban |
ProofWatch: Watchlist Guidance for Large Theories in E. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 270-288, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
1 | Bohua Zhan |
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 514-530, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava |
Certifying Standard and Stratified Datalog Inference Engines in SSReflect. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 171-188, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Dominik Kirst, Gert Smolka |
Categoricity Results for Second-Order ZF in Dependent Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 304-318, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Yannick Forster 0002, Gert Smolka |
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 189-206, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola |
A Verified Generational Garbage Collector for CakeML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 444-461, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler |
Efficient, Verified Checking of Propositional Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 269-284, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Cezary Kaliszyk, Josef Urban, Jirí Vyskocil |
Automating Formalization by Statistical and Semantic Parsing of Mathematics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 12-27, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Larchey-Wendling |
Typing Total Recursive Functions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 371-388, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Cyril Cohen, Damien Rouhling |
A Formal Proof in Coq of LaSalle's Invariance Principle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 148-163, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Julian Rosemann, Sigurd Schneider, Sebastian Hack |
Verified Spilling and Translation Validation with Repair. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 427-443, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Lochbihler |
Effect Polymorphism in Higher-Order Logic (Proof Pearl). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 389-409, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Raphaël Cauderlier, Catherine Dubois |
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 131-147, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Sophie Bernard |
Formalization of the Lindemann-Weierstrass Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 65-80, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Xavier Allamigeon, Ricardo D. Katz |
A Formalization of Convex Polyhedra Based on the Simplex Method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 28-45, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|