|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 1960 occurrences of 846 keywords
|
|
|
Results
Found 3383 publication records. Showing 3383 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
19 | Tadayuki Yoshida, Ekawit Nantajeewarawat, Masaharu Munetomo, Kiyoshi Akama |
Logical Approach to Theorem Proving with Term Rewriting on KR-logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
KEOD ![In: Proceedings of the 11th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management, IC3K 2019, Volume 2: KEOD, Vienna, Austria, September 17-19, 2019., pp. 282-289, 2019, ScitePress, 978-989-758-382-7. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan |
ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ARCH@CPSIoTWeek ![In: ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, part of CPS-IoT Week 2019, Montreal, QC, Canada, April 15, 2019., pp. 141-161, 2019, EasyChair. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Mark R. Greenstreet |
Integrating SMT with Theorem Proving for Verification of Analog and Mixed-Signal Circuits (Invited Tutorial). ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019, pp. 1, 2019, IEEE, 978-0-9835678-9-9. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Waqar Ahmad, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar |
On the formalization of importance measures using HOL theorem proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FormaliSE@ICSE ![In: Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019., pp. 109-118, 2019, IEEE / ACM, 978-1-7281-3373-7. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Daniel Huang 0001, Prafulla Dhariwal, Dawn Song, Ilya Sutskever |
GamePad: A Learning Environment for Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLR (Poster) ![In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019, 2019, OpenReview.net. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
19 | Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox |
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICML ![In: Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, pp. 454-463, 2019, PMLR. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
19 | Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson |
Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Vampire ![In: Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops, pp. 45-51, 2019, EasyChair. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
19 | Jonas Betzendahl |
Definedness Reasoning in Formal Mathematics and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM Workshops ![In: Joint Proceedings of the FMM and LML Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2019 co-located with the 12th Conference on Intelligent Computer Mathematics (CICM 2019), Prague, Czech Republic, July 8-12, 2019., 2019, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
19 | Fadil Kallat, Tristan Schäfer, Anna Vasileva |
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019., pp. 51-65, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Eunice Palmeira da Silva, Fred Freitas, Jens Otten |
Converting ALC Connection Proofs into ALC Sequents. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019., pp. 3-17, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Mathias Fleury, Hans-Jörg Schurr |
Reconstructing veriT Proofs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019., pp. 36-50, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui |
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019., pp. 27-35, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019., pp. 18-26, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Ludovic Font, Sébastien Cyr, Philippe R. Richard, Michel Gagnon |
Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@CADE ![In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019., pp. 1-16, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen |
Teaching a Formalized Logical Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@CADE ![In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019., pp. 73-92, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Nuno Baeta, Pedro Quaresma, Zoltán Kovács |
Towards a Geometry Automated Provers Competition. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@CADE ![In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019., pp. 93-100, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | David M. Cerna, Rafael P. D. Kiesel, Alexandra Dzhiganskaya |
A Mobile Application for Self-Guided Study of Formal Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@CADE ![In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019., pp. 35-53, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Josje Lodder, Bastiaan Heeren, Johan Jeuring |
Providing Hints, Next Steps and Feedback in a Tutoring System for Structural Induction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@CADE ![In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019., pp. 17-34, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | Sarah Winkler, Aart Middeldorp |
Tools in Term Rewriting for Education. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@CADE ![In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019., pp. 54-72, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | |
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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | Geoff Sutcliffe |
The 9th IJCAR Automated Theorem Proving System Competition - CASC-J9. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI Commun. ![In: AI Commun. 31(6), pp. 495-507, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Jan Jakubuv, Josef Urban |
Hierarchical invention of theorem proving strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI Commun. ![In: AI Commun. 31(3), pp. 237-250, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Zheng Yang 0007, Hang Lei |
Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 6, pp. 70331-70348, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | José de Jesús Lavalle-Martínez, Manuel Montes-y-Gómez, Héctor Jiménez-Salazar, Luis Villaseñor Pineda, Beatríz Beltrán Martínez |
Automatic Theorem Proving for Natural Logic: a Case Study on Textual Entailment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Computación y Sistemas ![In: Computación y Sistemas 22(1), 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Adnan Rashid, Osman Hasan |
Formal Analysis of Robotic Cell Injection Systems using Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1805.02858, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton |
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1806.03541, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Pasquale Minervini, Matko Bosnjak, Tim Rocktäschel, Sebastian Riedel 0001 |
Towards Neural Theorem Proving at Scale. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1807.08204, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Andres Campero, Aldo Pareja, Tim Klinger, Josh Tenenbaum 0001, Sebastian Riedel 0001 |
Logical Rule Induction and Theory Learning Using Neural Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1809.02193, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Mitsuru Kusumoto, Keisuke Yahata, Masahiro Sakai |
Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1811.00796, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Zheng Yang 0007, Hang Lei |
Optimization of Executable Formal Interpreters developed in Higher-order Theorem Proving Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1808.08511, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Pedro Quaresma, Walther Neuper (eds.) |
Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@CADE ![The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Michael Kinyon |
Proof Simplification and Automated Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1808.04251, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Daniel Huang 0001, Prafulla Dhariwal, Dawn Song, Ilya Sutskever |
GamePad: A Learning Environment for Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1806.00608, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák |
Reinforcement Learning of Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1805.07563, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Zheng Yang 0007, Hang Lei |
A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1803.00403, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu 0001, Gregor Snelting |
Introduction to Milestones in Interactive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 61(1-4), pp. 1-8, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Maria Paola Bonacina |
Parallel Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Handbook of Parallel Constraint Reasoning ![In: Handbook of Parallel Constraint Reasoning., pp. 179-235, 2018, Springer, 978-3-319-63515-6. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan |
ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ARCH@ADHS ![In: ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH@ADHS 2018, Oxford, UK, July 13, 2018, pp. 110-127, 2018, EasyChair. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Sumayya Shiraz, Osman Hasan |
Formal Verification of n-bit ALU Using Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBMF ![In: Formal Methods: Foundations and Applications - 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26-30, 2018, Proceedings, pp. 74-89, 2018, Springer, 978-3-030-03043-8. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | 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 |
|
19 | Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák |
Reinforcement Learning of Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NeurIPS ![In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada., pp. 8836-8847, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
19 | Yassmeen Elderhalli, Osman Hasan, Waqar Ahmad, Sofiène Tahar |
Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NFM ![In: NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings, pp. 139-156, 2018, Springer, 978-3-319-77934-8. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Alper Altuntas, John W. Baugh Jr. |
Hybrid Theorem Proving as a Lightweight Method for Verifying Numerical Software. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CORRECTNESS@SC ![In: 2nd IEEE/ACM International Workshop on Software Correctness for HPC Applications, CORRECTNESS@SC 2018, Dallas, TX, USA, November 12, 2018, pp. 1-8, 2018, IEEE, 978-1-7281-0226-9. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton |
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Haskell@ICFP ![In: Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2018, St. Louis, MO, USA, September 27-17, 2018, pp. 132-144, 2018, ACM, 978-1-4503-5835-4. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Yaqing Jiang, Petros Papapanagiotou, Jacques D. Fleuriot |
Machine Learning for Inductive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC ![In: Artificial Intelligence and Symbolic Computation - 13th International Conference, AISC 2018, Suzhou, China, September 16-19, 2018, Proceedings, pp. 87-103, 2018, Springer, 978-3-319-99956-2. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Walther Neuper |
Technologies for "Complete, Transparent & Interactive Models of Math" in Education. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@FLoC ![In: Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018., pp. 76-95, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Maximilian Doré, Krysia Broda |
Towards Intuitive Reasoning in Axiomatic Geometry. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@FLoC ![In: Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018., pp. 38-55, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Nuno Baeta, Pedro Quaresma |
Towards Ranking Geometric Automated Theorem Provers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@FLoC ![In: Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018., pp. 30-37, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Wolfgang Schreiner |
Theorem and Algorithm Checking for Courses on Logic and Formal Methods. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@FLoC ![In: Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018., pp. 56-75, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Jørgen Villadsen, Asta Halkjær From, Anders Schlichtkrull |
Natural Deduction Assistant (NaDeA). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@FLoC ![In: Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018., pp. 14-29, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | Anders Schlichtkrull, Jørgen Villadsen, Asta Halkjær From |
Students' Proof Assistant (SPA). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@FLoC ![In: Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018., pp. 1-13, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
19 | 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 |
|
|
|