On the adequacy of representing higher order intuitionistic logic as a pure type system
DOI10.1016/0168-0072(92)90044-ZzbMATH Open0763.03007WikidataQ126352769 ScholiaQ126352769MaRDI QIDQ1194249FDOQ1194249
Authors: Hans Tonino, Ken-etsu Fujita 
Publication date: 27 September 1992
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
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
proof treescalculus of constructionspure type systemCurry-Howard-De Bruijn isomorphismhigher order many sorted intuitionistic predicate logic
Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)
Cites Work
Cited In (6)
- On the conservativity of Leibniz equality
- Equivalences between pure type systems and systems of illative combinatory logic
- Conservativity between logics and typed λ calculi
- Weak normalization implies strong normalization in a class of non-dependent pure type systems
- (In)consistency of Extensions of Higher Order Logic and Type Theory
- Predicates as types
Uses Software
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)
