Syntactic analysis of \(\eta\)-expansions in pure type systems.

DOI10.1016/S0890-5401(03)00019-1zbMath1037.68037MaRDI QIDQ1873755

Felix Joachimski

Publication date: 27 May 2003

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

simply typed \(\lambda\)-calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• Operational aspects of untyped Normalisation by Evaluation

This page was built for publication: Syntactic analysis of \(\eta\)-expansions in pure type systems.