Guarded Homotopy Type Theory (GHoTT)

In this project we investigate guarded homotopy type theory, a new type theory encompassing features of homotopy type theory and guarded recursion. The aim is to develop new theory and prototype implementations of a new generation of proof assistants, which can be used for both mathematics and program verification.

The project is funded by the Villum Foundation, 2015-2019.

People at Aarhus

Publications

Multimodal Dependent Type Theory
D. Gratzer, G.A. Kavvos, A. Nuyts, and L. Birkedal
Submitted for publication (ArXiv: 2011.15021). Journal version of LICS 2020 paper.
.pdf
Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
S. Spies, L. Gaher, D. Gratzer, J. Tassarotti, R. Krebbers, D. Dreyer, and L. Birkedal
Submitted for publication.
.pdf
Multimodal Dependent Type Theory
D. Gratzer, G. A. Kavvos, A. Nuyts, and L. Birkedal
In LICS 2020: Logic in Computer Science
.pdf
A Cubical Language for Cubical Bishop Sets
J. Sterling, C. Angiuli, and D. Gratzer
Submitted for publication
[preprint] .pdf
A Quantum of Direction
G.A. Kavvos
Submitted for publication
[preprint] .pdf
Synthetic topology in Homotopy Type Theory for probabilistic programming
M.E. Bidlingmaier, F. Faissole, and B. Spitters
Submitted for publication (arXiv:1912.07339)
[preprint] .pdf
An Application of Computable Distributions to the Semantics of Probabilistic Programs
D. Huang, G. Morrisett, B. Spitters
In Foundations of Probabilistic Programming, ed. Gilles Barthe, Joost-Pieter Katoen & Alexandra Silva, Cambridge University Press, 2020
[preprint] .pdf
Modalities in Homotopy Type Theory
E. Rijke, M. Shulman, B. Spitters
Logical Methods in Computer Science, January 2020, Volume 16, Issue 1
.pdf
Cubical Syntax for Reflection-Free Extensional Equality
J. Sterling, C. Angiuli, and D. Gratzer
In FSCD 2019: Formal Structures for Computation and Deduction
Recipient of Best Paper Award for Junior Researchers
.pdf
Implementing a Modal Dependent Type Theory
D. Gratzer, J. Sterling, and L. Birkedal
In ICFP 2019: International Conference on Functional Programming, Berlin, Germany
Recipient of ICFP 2019 Distinguished Paper Award
.pdf technical appendix
Modal Dependent Type Theory and Dependent Right Adjoints
L. Birkedal, R. Clouston, B. Mannaa, R.E. Møgelberg, A.M. Pitts, and B. Spitters
Mathematical Structures in Computer Science 1-21, 2019
.pdf
Guarded Cubical Type Theory
L. Birkedal, A. Bizjak, R. Clouston, H.B. Grathwohl, B. Spitters, and A. Vezzosi
Journal of Automated Reasoning 63(2): 211--253, 2019
.pdf
Internal Universes in Models of Homotopy Type Theory
D.R. Licata, I. Orton, A.M. Pitts,B. Spitters
In FSCD 2018: Formal Structures for Computation and Deduction
.pdf
Fitch-Style Modal Lambda Calculi
R. Clouston
In FOSSACS 2018: Foundations of Software Science and Computation Structures
.pdf
A Model of Guarded Recursion via Generalised Equilogical Spaces
A. Bizjak and L. Birkedal
Theoretical Computer Science, 772:1–18, 2018
.pdf
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
A. Aguirre, G. Barthe, L. Birkedal, A. Bizjak, M. Gaboardi, and D. Garg
In ESOP 2018: European Symposium on Programming
.pdf
On Models of Higher-Order Separation Logic
A. Bizjak and L. Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics
.pdf
The HoTT Library: A formalization of homotopy type theory in Coq
A. Bauer, J. Gross, P. Lumsdaine, M. Shulman, M. Sozeau, B. Spitters
In CPP 2017: Certified Proofs and Programs
.pdf
The clocks are ticking: no more delays!
P. Bahr, H.B. Grathwohlk, R.E. Mogelberg
In LICS 2017: Logic in Computer Science
.pdf
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
L. Birkedal, A. Bizjak, R. Clouston, H.B. Grathwohl, B. Spitters, and A. Vezzosi
In CSL 2016: Computer Science Logic
.pdf
The Guarded Lambda Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
R. Clouston, A. Bizjak, H. Bugge Grathwohl, and L. Birkedal
Logical Methods in Computer Science, 2016.
Journal version of FOSSACS 2015 paper
.pdf
Guarded Cubical Type Theory
L. Birkedal, A. Bizjak, R. Clouston, H.B. Gratwohl, B. Spitters, and A. Vezzosi.
In TYPES 2016
.pdf
Guarded Dependent Type Theory with Coinductive Types
A. Bizjak, H.B. Grathwohl, R. Clouston, R.E. Møgelberg, and L. Birkedal
In FOSSACS 2016: Foundations of Software Science and Computation Structures
.pdf
A Model of PCF in Guarded Type Theory
M. Paviotti, R.E. Møgelberg, and L. Birkedal
In MFPS 2015: Mathematical Foundations of Programming Semantics
.pdf
Programming and Reasoning with Guarded Recursion for Coinductive Types
R. Clouston, A. Bizjak, H. Bugge Grathwohl, and L. Birkedal
In FOSSACS 2015: Foundations of Software Science and Computation Structures
.pdf