Logic Programming and Type Inference with the Calculus of Constructions

For my grandfather. iv In this thesis I present a higher order logic programming language, Cale-don, with a pure type system and a Turing complete type inference and im-plicit 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 tech-niques which are normally either unavailable or only possible with second thought extensions. The addition of control structures such as implicit ar-guments, shared holes, polymorphism, and nondeterminism control makes programming computation during type inference more natural. As a conse