A unified approach to type theory through a refined \(\lambda\)-calculus

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

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40)

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

• Automath

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