A linearization of the Lambda-calculus and consequences

DOI10.1093/logcom/10.3.411zbMath0953.03014OpenAlexW2002689571MaRDI QIDQ4500177

A. J. Kfoury

Publication date: 4 September 2000

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://hdl.handle.net/2144/1597

zbMATH Keywords

weak normalization\(\lambda\)-calculusintersection typesstrong normalizationtype inferencegeneralization of beta reduction

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (21)

A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization ⋮ Parsimonious Types and Non-uniform Computation ⋮ Unnamed Item ⋮ Differential interaction nets ⋮ Execution time of λ-terms via denotational semantics and intersection types ⋮ Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) ⋮ Structural rules and algebraic properties of intersection types ⋮ Quantitative weak linearisation ⋮ Node Replication: Theory And Practice ⋮ Tight typings and split bounds, fully developed ⋮ Unnamed Item ⋮ The spirit of node replication ⋮ Uniformity and the Taylor expansion of ordinary lambda-terms ⋮ Intuitionistic differential nets and lambda-calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Reasoning About Call-by-need by Means of Types ⋮ Weak linearization of the lambda calculus ⋮ Infinitary affine proofs ⋮ Essential and relational models

This page was built for publication: A linearization of the Lambda-calculus and consequences