Volume 63, Issue 2

Search all Journal of Automated Reasoning articles

August 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

Issue Editors:

Peter Lefanu Lumsdaine,
Nicolas Tabareau,
Mauricio Ayala-Rincón,
César Muñoz

16 articles in this issue

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations
Peter Lefanu Lumsdaine
Nicolas Tabareau
EditorialNotes 30 October 2018 Pages: 157 - 158
The Univalence Axiom in Cubical Sets
Marc Bezem
Thierry Coquand
Simon Huber
OriginalPaper Open access 26 June 2018 Pages: 159 - 171
Canonicity for Cubical Type Theory
Simon Huber
OriginalPaper Open access 13 June 2018 Pages: 173 - 210
Guarded Cubical Type Theory
Lars Birkedal
Aleš Bizjak
Andrea Vezzosi
OriginalPaper 26 June 2018 Pages: 211 - 253
The James Construction and \(\pi _4(\mathbb {S}^{3})\) in Homotopy Type Theory
Guillaume Brunerie
OriginalPaper 27 June 2018 Pages: 255 - 284
From Signatures to Monads in UniMath
Benedikt Ahrens
Ralph Matthes
Anders Mörtberg
OriginalPaper Open access 11 July 2018 Pages: 285 - 318
Selected Extended Papers of ITP 2017
Mauricio Ayala-Rincón
César Muñoz
EditorialNotes 04 December 2018 Pages: 319 - 321
A Formalization of Convex Polyhedra Based on the Simplex Method
Xavier Allamigeon
Ricardo D. Katz
OriginalPaper 04 August 2018 Pages: 323 - 345
A Formal Proof of the Expressiveness of Deep Learning
Alexander Bentkamp
Jasmin Christian Blanchette
Dietrich Klakow
OriginalPaper Open access 22 September 2018 Pages: 347 - 368
CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics
Frédéric Besson
Sandrine Blazy
Pierre Wilke
OriginalPaper 16 November 2018 Pages: 369 - 392
Call-by-Value Lambda Calculus as a Model of Computation in Coq
Yannick Forster
Gert Smolka
OriginalPaper 19 October 2018 Pages: 393 - 413
Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory
Dominik Kirst
Gert Smolka
OriginalPaper 11 October 2018 Pages: 415 - 438
Effect Polymorphism in Higher-Order Logic (Proof Pearl)
Andreas Lochbihler
OriginalPaper 10 July 2018 Pages: 439 - 462
A Verified Generational Garbage Collector for CakeML
Adam Sandberg Ericsson
Magnus O. Myreen
Johannes Åman Pohjola
OriginalPaper Open access 03 November 2018 Pages: 463 - 488
Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology
Yannick Zakowski
David Cachera
Jan Vitek
OriginalPaper 01 November 2018 Pages: 489 - 515
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2
Bohua Zhan
OriginalPaper 02 August 2018 Pages: 517 - 538

Volume 63, Issue 2

Search

Navigation