Reduction rules for intuitionistic -calculus

DOI10.1007/S11225-015-9616-1MaRDI QIDQ897480zbMATH OpenOpenAlexFDO

Authors Ken-etsu Fujita, Ryo Kashima, Naosuke Matsuda, 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)

Recommendations

• \(\lambda \rho\)-calculus. II
• scientific article; zbMATH DE number 2024631
• scientific article; zbMATH DE number 2095713
• The Intensional Lambda Calculus
• An estimation for the lengths of reduction sequences of the \(\lambda\mu\rho\theta\)-calculus

Cites work

• scientific article; zbMATH DE number 5318491 (Why is no real title available?)
• scientific article; zbMATH DE number 1305942 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 2242601 (Why is no real title available?)
• A \(\rho\)-calculus of explicit constraint application
• A simplified proof of the Church-Rosser theorem
• Lectures on the Curry-Howard isomorphism
• Monad as modality
• \(\lambda \rho\)-calculus. II

Cited in

(8)

• scientific article; zbMATH DE number 1523050 (Why is no real title available?)
• scientific article; zbMATH DE number 176742 (Why is no real title available?)
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• scientific article; zbMATH DE number 1303339 (Why is no real title available?)
• Reduction and introducers in \(d\)-contexts
• scientific article; zbMATH DE number 2024631 (Why is no real title available?)
• Reducibility Proofs in the λ-Calculus
• \(\lambda \rho\)-calculus. II

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

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