Skip to main content


Journal of Automated Reasoning

Journal of Automated Reasoning 2/2019

Issue 2/2019

Special Issue: Homotopy Type Theory and Univalent Foundations / Guest Editors: Peter Lefanu Lumsdaine, Nicolas Tabareau & Special Issue: Selected Extended Papers of ITP 2017 / Guest Editors: Mauricio Ayala-Rincón, César Muñoz

Table of Contents ( 16 Articles )

30-10-2018 | Issue 2/2019

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations

Peter Lefanu Lumsdaine, Nicolas Tabareau

26-06-2018 | Issue 2/2019 Open Access

The Univalence Axiom in Cubical Sets

Marc Bezem, Thierry Coquand, Simon Huber

13-06-2018 | Issue 2/2019 Open Access

Canonicity for Cubical Type Theory

Simon Huber

26-06-2018 | Issue 2/2019

Guarded Cubical Type Theory

Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi

27-06-2018 | Issue 2/2019

The James Construction and in Homotopy Type Theory

Guillaume Brunerie

11-07-2018 | Issue 2/2019 Open Access

From Signatures to Monads in UniMath

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

04-12-2018 | Issue 2/2019

Selected Extended Papers of ITP 2017

Mauricio Ayala-Rincón, César Muñoz

04-08-2018 | Issue 2/2019

A Formalization of Convex Polyhedra Based on the Simplex Method

Xavier Allamigeon, Ricardo D. Katz

22-09-2018 | Issue 2/2019 Open Access

A Formal Proof of the Expressiveness of Deep Learning

Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow

16-11-2018 | Issue 2/2019

CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics

Frédéric Besson, Sandrine Blazy, Pierre Wilke

19-10-2018 | Issue 2/2019

Call-by-Value Lambda Calculus as a Model of Computation in Coq

Yannick Forster, Gert Smolka

11-10-2018 | Issue 2/2019

Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory

Dominik Kirst, Gert Smolka

10-07-2018 | Issue 2/2019

Effect Polymorphism in Higher-Order Logic (Proof Pearl)

Andreas Lochbihler

03-11-2018 | Issue 2/2019 Open Access

A Verified Generational Garbage Collector for CakeML

Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola

01-11-2018 | Issue 2/2019

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

02-08-2018 | Issue 2/2019

Formalization of the Fundamental Group in Untyped Set Theory Using Auto2

Bohua Zhan

Current Publications

Premium Partner

    Image Credits