Dependently Typed Higher-Order Logic

What? Why?

Syntax

Resources