Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types

DOI10.1007/978-3-642-19805-2_7zbMath1326.68067OpenAlexW191576729MaRDI QIDQ3000601

Alexis Bernadet, Stéphane Lengrand

Publication date: 19 May 2011

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19805-2_7

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (9)

A semantic account of strong normalization in linear logic ⋮ A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization ⋮ Call-by-Value Non-determinism in a Linear Logic Type Discipline ⋮ Unnamed Item ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Tight typings and split bounds, fully developed ⋮ Strong normalization through intersection types and memory ⋮ Unnamed Item ⋮ Essential and relational models

This page was built for publication: Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types