Programming with Higher-Order Logic

A programming language based on a higher-order logic provides a declarative approach to capturing computations involving types, proofs and other syntactic structures.