A linearization of the Lambda-calculus and consequences
From MaRDI portal
Publication:4500177
DOI10.1093/logcom/10.3.411zbMath0953.03014OpenAlexW2002689571MaRDI QIDQ4500177
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
weak normalization\(\lambda\)-calculusintersection typesstrong normalizationtype inferencegeneralization of beta reduction
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