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
Random question but do you know a good reference (beyond elaboration zoo) for how to do elaboration of metas in this set up?
2
Yeah I've found it's a bit tricky to find self-contained resources for solving metavariables, so the barrier to entry is quite high. "Elaboration with First-Class Implicit Function Types" came out recently though, and I was hoping to try implementing it: icfp20.sigplan.org/details/icfp-2