Dependently Typed Higher-Order Logic
What? Why?
- HOL with types that take term arguments.
- Type checking undecidable
- Elegant definition of data structures
- Translation to HOL
Syntax
- Use the !> polymorphic binder for types
- Dependent types declared with terms and types
- Instantiations apply terms to dependent types
- An example problem
Resources