Normalization by evaluation with typed abstract syntax