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
Replying to
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 😅
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! 😅
1
I found exactly the same thing, I wonder abstractly why, roughly the reason is because indices are good for deconstructing terms and levels for reconstructing in terms of sharing but it would be nice to have an abstract reason.
1
1
Yeah, seems to be something like that! Here is a neat post by on the indices+levels approach as well: colimit.net/posts/normalis
1
3
Show replies