I want to implement a cubical type theory based proof assistant from scratch. Any pointers for how to get started? There's a good research reason for this
10
6
58
Conversation
williamjbowman.com/#depmacros
Can't help with the cubical part, but we've got some infrastructure for quickly building (dependently) typed languages
1
9
It is going to be in Rust, which I'm sure sounds crazy but there's a reason for it
8
15
You might find this helpful (current project I'm playing with) github.com/pikelet-lang/p
2
2
Note that the 'next' branch is far further ahead than the main branch - rebuilding it using normalisation by evaluation as alluded to on my other thread: github.com/pikelet-lang/p