A note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments

DOI10.1016/j.ipl.2013.07.027zbMath1329.68067OpenAlexW2024485337MaRDI QIDQ2350605

Aleksy Schubert, Ken-etsu Fujita

Publication date: 25 June 2015

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2013.07.027

zbMATH Keywords

formal semanticstype systemsabstract data typesexistential quantifiersubject reduction

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Lectures on the Curry-Howard isomorphism
• Intersection and union types: Syntax and semantics
• Existential Type Systems with No Types in Terms
• Residual theory in λ-calculus: a formal development
• On the Stability by Union of Reducibility Candidates

This page was built for publication: A note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments