On the adequacy of representing higher order intuitionistic logic as a pure type system

DOI10.1016/0168-0072(92)90044-ZzbMath0763.03007WikidataQ126352769 ScholiaQ126352769MaRDI QIDQ1194249

Hans Tonino, Ken-etsu Fujita

Publication date: 27 September 1992

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

calculus of constructionsproof treespure type systemCurry-Howard-De Bruijn isomorphismhigher order many sorted intuitionistic predicate logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items

Conservativity between logics and typed λ calculi ⋮ Weak normalization implies strong normalization in a class of non-dependent pure type systems ⋮ ON THE CONSERVATIVITY OF LEIBNIZ EQUALITY

Uses Software

• Automath

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item