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
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
2
Random question but do you know a good reference (beyond elaboration zoo) for how to do elaboration of metas in this set up?
2
Separately I think Pikelet sounds super interesting, did you have any particular inspirations on the systems programming/ low-level side of things?
1
Show replies