mortberg/cubicaltt
View on GitHub ↗ ★ 610 Haskell
Experimental implementation of Cubical Type Theory
4 mentions on Hacker News by 4 people: 1 story, 3 comments · first 2015-07-11 · latest 2017-10-31
20082026
-
Cubical https://github.com/mortberg/cubicaltt is a proof of concept programming language based on constructive (cubical type theory https://arxiv.org/abs/1611.02108 ) interpretation of HoTT. Agda also added recently support for cubical…
comment by hiker · 2017-10-31 · in Simplicity: A New Language for Blockchains [pdf] -
…having to learn anything about homotopy theory, though the intuition will probably help. [1] https://github.com/mortberg/cubicaltt
comment by maxiepoo · 2017-02-05 · in Ask HN: What is the most exciting development in your field right now? -
…there are already some experimental implementations that can do some magic, for example this one: https://github.com/mortberg/cubicaltt
comment by Kutta · 2015-07-11 · in Relation Between Type Theory, Category Theory and Logic