yacctt: Yet Another Cartesian Cubical Type Theory
Haskell
77
162 commits
updated Jul 30, 2018
This is an extremely experimental implementation of a cartesian cubical type theory based on https://arxiv.org/abs/1712.01800 written by Anders Mörtberg and Carlo Angiuli. It is mainly meant as proof of concept and for experimentation with new cubical features and ideas.
It is based on the code base of https://github.com/mortberg/cubicaltt/.
Haskell
91.5%
Emacs Lisp
6.0%
Makefile
2.5%
yacctt: Yet Another Cartesian Cubical Type Theory
Haskell
77
162 commits
updated Jul 30, 2018
This is an extremely experimental implementation of a cartesian cubical type theory based on https://arxiv.org/abs/1712.01800 written by Anders Mörtberg and Carlo Angiuli. It is mainly meant as proof of concept and for experimentation with new cubical features and ideas.
It is based on the code base of https://github.com/mortberg/cubicaltt/.
Haskell
91.5%
Emacs Lisp
6.0%
Makefile
2.5%