DOTter

(Mostly) Agda¹ and Coq developments and experiments on dependent object types (DOT) and related systems.

Contents

• nbe/ Normalization by Evaluation (NbE) for DOT/System D calculi with full(er) dependent types.

• logrel/ Strong normalization of DOT calculi using logical relations.

¹_{Dotter is German for egg yolk.}