Examples

• Palindromes
• Binary Search Trees
• A Certified Type Checker
• The Well-Typed Interpreter
• Dependent de Bruijn Indices
• Parametric Higher-Order Abstract Syntax