Reduction rules for intuitionistic \(\lambda\rho\)-calculus

DOI10.1007/s11225-015-9616-1zbMath1378.03012OpenAlexW851658754MaRDI QIDQ897480

Ryo Kashima, Naosuke Matsuda, Ken-etsu Fujita, Yuichi Komori

Publication date: 7 December 2015

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11225-015-9616-1

zbMATH Keywords

proof theoryintuitionistic logicCurry-Howard isomorphism\(\lambda\rho\)-calculus

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Cites Work

• Lectures on the Curry-Howard isomorphism
• Monad as modality
• A simplified proof of the Church-Rosser theorem
• \(\lambda \rho\)-calculus. II
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Reduction rules for intuitionistic \(\lambda\rho\)-calculus