In this thesis I present a higher order logic programming language, Caledon, with a pure type system and a Turing complete type inference and implicit argument system based on the same logic programming semantics. Because the language has dependent types and type inference, terms can be generated by providing type constraints. I design the dynamic semantics of this language to be the same used to perform type inference, such that there is no disparity between compilation and running. The lack of distinction between compilation and execution permits certain metaprogramming techniques which are normally either unavailable or only possible with second thought extensions. The addition of control structures such as implicit arguments, shared holes, polymorphism, and nondeterminism control makes programming computation during type inference more natural. As a consequence of these extensions, unification problems must be generated to solve for terms in addition to the usual problems generated to solve for types. Furthermore, because every result of execution is a term in the consistent calculus of constructions, Caledon can be considered an interactive theorem prover with a less orthogonal combination of proof search and proof checking than has previously been designed or implemented.

104 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by [email protected]