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

Selected Related Publications:

L. Birkedal, A. Bizjak, R. Clouston, H.B. Grathwohl, B. Spitters, and A. Vezzosi. Guarded cubical type theory. Journal of Automated Reasoning, special issue of HoTT/UF, 2018. (PDF)

D.R. Licata, I. Orton, A.M. Pitts,B. Spitters. Internal Universes in Models of Homotopy Type Theory. Proceedings of FSCD 2018, 2018. (PDF)

R. Clouston. Fitch-Style Modal Lambda Calculi. Proceedings of FOSSACS 2018, 2018. (PDF)

E. Rijke, M. Shulman, B. Spitters. Modalities in Homotopy Type Theory. To Appear in LMCS, 2018. (PDF)

A. Bizjak and L. Birkedal. A model of guarded recursion via generalised equilogical spaces. Theoretical Computer Science, 772:1-18, 2018. (PDF)

A. Aguirre, G. Barthe, L. Birkedal, A. Bizjak, M. Gaboardi, and D. Garg. Relational reasoning for Markov chains in a probabilistic guarded lambda calculus. In Proceedings of ESOP 2018, 2018. (PDF)

A. Bizjak and L. Birkedal. On models of higher-order separation logic. In Proceedings of MFPS2017, 2017. (PDF)

A. Bauer, J. Gross, P. Lumsdaine, M. Shulman, M. Sozeau, B. Spitters. The HoTT Library: A formalization of homotopy type theory in Coq. In Proceedings of CPP2017, 2017. (PDF)

P. Bahr, H.B. Grathwohlk, R.E. Mogelberg. The clocks are ticking: no more delays!. Proceedings of LICS, 2017. (PDF)

R. Clouston, A. Bizjak, H. Bugge Grathwohl, and L. Birkedal. The guarded lambda calculus: Programming and reasoning with guarded recursion for coinductive types. Logical Methods in Computer Science, 2016. Accepted for publication (journal version of FOSSACS 2015 paper). (PDF)

L. Birkedal, A. Bizjak, R. Clouston, H.B. Gratwohl, B. Spitters, and A. Vezzosi. Guarded cubical type theory. In Proceedings of Types 2016, 2016. (PDF)

A. Bizjak, H.B. Grathwohl, R. Clouston, R.E. Møgelberg, and L. Birkedal. Guarded dependent type theory with coinductive types. In Proceedings of FOSSACS 2016, 2016. (PDF)

M. Paviotti, R.E. Møgelberg, and L. Birkedal. A model of PCF in guarded type theory. In Proocedings of MFPS, 2015. (PDF)

R. Clouston, A. Bizjak, H. Bugge Grathwohl, and L. Birkedal. Programming and reasoning with guarded recursion for coinductive types. In Proceedings of FOSSACS, 2015. (PDF)