3 ms·
This is an interesting idea but is there any description of the soundness of this approach? Any functionality capable of subsuming not just inductive types but
by the_french 5y ago
This is an interesting idea but is there any description of the soundness of this approach? Any functionality capable of subsuming not just inductive types but higher-inductive types is going to be very subtle. I looked around on the repository but I can't find any formal description of the language or type theory, which is worrying for a proof tool.
- skybrian 5y agoThe plan for Kind itself seems to be to allow possibly unsound expressions (for example that don’t terminate), but to have consistency checkers. See: https://github.com/kind-lang/Kind/blob/master/CONTRIBUTE.md#add-a-consistency-checker https://github.com/kind-lang/Kind/blob/master/CONTRIBUTE.md#...
- logicchains 5y agoThere's a paper on the soundness of self types: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...