Dependence and independence results for (impredicative) calculi of dependent types

DOI10.1017/S0960129500001122zbMath0749.03054MaRDI QIDQ4006238

Thomas Streicher

Publication date: 26 September 1992

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

independencedependencecategorical semantics\(\text{PER} \omega\) modelimpredicative calculi of dependent typessub-locally- Cartesian-closed category

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Independence of the induction principle and the axiom of choice in the pure calculus of constructions

Cites Work

• Locally cartesian closed categories and type theory

This page was built for publication: Dependence and independence results for (impredicative) calculi of dependent types