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

DOI10.1016/0168-0072(92)90044-ZMaRDI QIDQ1194249zbMATH OpenWikidataFDO

Authors 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

proof treescalculus of constructionspure 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)

Recommendations

• Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• Equivalences between pure type systems and systems of illative combinatory logic
• scientific article; zbMATH DE number 1377703
• Intensional logic and two-sorted type theory
• scientific article; zbMATH DE number 45491
• scientific article; zbMATH DE number 516994
• Computational adequacy for recursive types in models of intuitionistic set theory
• scientific article; zbMATH DE number 512782
• Higher-Order Logic and Type Theory

Cites work

• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 194511 (Why is no real title available?)
• scientific article; zbMATH DE number 1400716 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(7)

• On the conservativity of Leibniz equality
• Equivalences between pure type systems and systems of illative combinatory logic
• Conservativity between logics and typed λ calculi
• Automata theory approach to predicate intuitionistic logic
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• Weak normalization implies strong normalization in a class of non-dependent pure type systems
• Predicates as types

Describes a project that uses

Uses Software

• Automath

This page was built for publication: On the adequacy of representing higher order intuitionistic logic as a pure type system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1194249)