Reduction rules for intuitionistic -calculus

DOI10.1007/S11225-015-9616-1zbMATH Open1378.03012OpenAlexW851658754MaRDI QIDQ897480FDOQ897480

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

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

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

• Title not available (Why is that?)
• Title not available (Why is that?)
• Lectures on the Curry-Howard isomorphism
• Title not available (Why is that?)
• Monad as modality
• A simplified proof of the Church-Rosser theorem
• Title not available (Why is that?)
• \(\lambda \rho\)-calculus. II
• A \(\rho\)-calculus of explicit constraint application
• Title not available (Why is that?)

Cited In (7)

• Title not available (Why is that?)
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• Title not available (Why is that?)
• Reduction and introducers in \(d\)-contexts
• Title not available (Why is that?)
• Reducibility Proofs in the λ-Calculus
• Title not available (Why is that?)

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)