mortberg/yacctt

yacctt: Yet Another Cartesian Cubical Type Theory

Haskell

77

162 commits

updated Jul 30, 2018

See the code

README

yacctt: Yet Another Cartesian Cubical Type Theory

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/.

Contributors

mortberg

144 commits

cangiuli

17 commits

5HT

1 commits

mortberg/yacctt

yacctt: Yet Another Cartesian Cubical Type Theory

Haskell

77

162 commits

updated Jul 30, 2018

See the code

README

yacctt: Yet Another Cartesian Cubical Type Theory

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/.

Contributors

mortberg

144 commits

cangiuli

17 commits

5HT

1 commits

Languages

Haskell

91.5%

Emacs Lisp

6.0%

Makefile

2.5%