• root

• blog/
• cv
• misc/

1 The problem of romalization

2 Toy example

3 NbE for the toy example

4 Proving normalization correctness

4.1 Soundness

4.2 Completeness