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
I haven’t done cubical stuff yet, but in doing dependently typed languages I’ve found normalisation-by-evaluation with debruijn indicies in terms and debruijn levels in values to be a pretty good starting point! You might already be on top of that stuff though 😅
2
4
The advantage of doing it this way is it's pretty simple to implement and seems to perform pretty well. You can then make alterations to further improve performance later.
1
I say this because I did a big detour around locally nameless an unbound and wish somebody else had pointed me in this direction earlier! 😅