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
A Cubical Language for Cubical Bishop Sets
J. Sterling, C. Angiuli, and D. Gratzer
Submitted for publication
A Quantum of Direction
G.A. Kavvos
Submitted for publication
Synthetic topology in Homotopy Type Theory for probabilistic programming
M.E. Bidlingmaier, F. Faissole, and B. Spitters
Submitted for publication
An Application of Computable Distributions to the Semantics of Probabilistic Programs
D. Huang, G. Morrisett, B. Spitters
Accepted for publication in Foundations of Probabilistic Programming
Modalities in Homotopy Type Theory
E. Rijke, M. Shulman, B. Spitters
Logical Methods in Computer Science, January 2020, Volume 16, Issue 1
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
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
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
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
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
Fitch-Style Modal Lambda Calculi
R. Clouston
In FOSSACS 2018: Foundations of Software Science and Computation Structures
A Model of Guarded Recursion via Generalised Equilogical Spaces
A. Bizjak and L. Birkedal
Theoretical Computer Science, 772:1–18, 2018
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
On Models of Higher-Order Separation Logic
A. Bizjak and L. Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics
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
The clocks are ticking: no more delays!
P. Bahr, H.B. Grathwohlk, R.E. Mogelberg
In LICS 2017: Logic in Computer Science
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
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
Guarded Cubical Type Theory
L. Birkedal, A. Bizjak, R. Clouston, H.B. Gratwohl, B. Spitters, and A. Vezzosi.
In TYPES 2016
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
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
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