Skip to main content


Journal of Automated Reasoning

Journal of Automated Reasoning 5/2020

Issue 5/2020

Special Issue: Selected Extended Papers from ITP 2018

Table of Contents ( 7 Articles )

22-05-2020 | Issue 5/2020

Preface: Selected Extended Papers from Interactive Theorem Proving 2018

Jeremy Avigad, Assia Mahboubi

31-01-2020 | Issue 5/2020

Graph Theory in Coq: Minors, Treewidth, and Isomorphisms

Christian Doczkal, Damien Pous

09-06-2020 | Issue 5/2020 Open Access

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL

René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada

10-12-2019 | Issue 5/2020 Open Access

A Relaxation of Üresin and Dubois’ Asynchronous Fixed-Point Theory in Agda

Matthew L. Daggitt, Ran Zmigrod, Timothy G. Griffin

08-02-2020 | Issue 5/2020 Open Access

Verified Analysis of Random Binary Tree Structures

Manuel Eberl, Max W. Haslbeck, Tobias Nipkow

18-01-2020 | Issue 5/2020

Formal Reasoning Under Cached Address Translation

Hira Taqdees Syeda, Gerwin Klein

18-02-2020 | Issue 5/2020

The MetaCoq Project

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter

Current Publications

Premium Partner

    Image Credits