A unified approach to type theory through a refined \(\lambda\)-calculus
From MaRDI portal
Publication:1349674
DOI10.1016/0304-3975(94)00127-5zbMath0874.03014OpenAlexW2000972984MaRDI QIDQ1349674
Fairouz Kamareddine, Rob Nederpelt
Publication date: 27 February 1997
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(94)00127-5
Related Items
A unified approach to type theory through a refined \(\lambda\)-calculus ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ A useful \(\lambda\)-notation ⋮ Refining reduction in the lambda calculus ⋮ Canonical typing and ∏-conversion in the Barendregt Cube ⋮ THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES
Uses Software
Cites Work
- Needed reduction and spine strategies for the lambda calculus
- The calculus of constructions
- A system at the cross-roads of functional and logic programming
- Nominalization, predication and type containment
- \(\lambda\)-terms, logic, determiners and quantifiers
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- A unified approach to type theory through a refined \(\lambda\)-calculus
- A useful \(\lambda\)-notation
- ON STEPWISE EXPLICIT SUBSTITUTION
- Refining reduction in the lambda calculus
- Canonical typing and ∏-conversion in the Barendregt Cube
- Set Theory and Nominalization, Part I
- Set Theory and Nominalization, Part II
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item