Examples

• A Certified Type Checker
• The Well-Typed Interpreter
• Dependent de Bruijn Indices