A general method for proving the normalization theorem for first and second order typed λ-calculi

DOI10.1017/S0960129599002923zbMath0942.03017OpenAlexW2010737695MaRDI QIDQ4946629

Silvio Valentini, Venanzio Capretta

Publication date: 23 August 2000

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129599002923

zbMATH Keywords

typed lambda-calculusnormalization propertyGirard's system F

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (2)

A binary modal logic for the intersection types of lambda-calculus. ⋮ Perpetual reductions in \(\lambda\)-calculus

Uses Software

• Automath

This page was built for publication: A general method for proving the normalization theorem for first and second order typed λ-calculi