GADTs

tags:
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