Semantics of Type Theory: Correctness, Completeness and Independence Results
Thomas Streicher · Medical Entomology and Zoology · 1991
An exploration of the categorical semantics of theories of dependent and polymorphic types, using the example of Coquand and Huet's calculus of constructions. The application of constructive mathematics to the problem of defining functional computer programming languages should interest mathematicia