root
cv
misc/
GADTs
tags:
coq
gadt
ocaml
haskell
Discussing models of GADTs and why it's hard to relate shapes and gears
posted on May 5, 2024
Table of Contents
1
The problem of romalization
2
Toy example
3
NbE for the toy example
4
Proving normalization correctness
4.1
Soundness
4.2
Completeness
1
The problem of romalization
2
Toy example
3
NbE for the toy example
4
Proving normalization correctness
4.1
Soundness
4.2
Completeness