Non-idempotent intersection types and strong normalisation

DOI10.2168/LMCS-9(4:3)2013zbMath1297.03010arXiv1310.1622OpenAlexW2001822718MaRDI QIDQ2851671

Alexis Bernadet, Stéphane Lengrand

Publication date: 16 October 2013

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1310.1622

zbMATH Keywords

complexityfiltersintersection typesstrong normalisationnon-idempotenceorthogonality models

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)

Related Items (16)

A semantic account of strong normalization in linear logic ⋮ Unnamed Item ⋮ Nominal essential intersection types ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Tight typings and split bounds, fully developed ⋮ Normal-order reduction grammars ⋮ Unnamed Item ⋮ Strong normalization through intersection types and memory ⋮ The vectorial \(\lambda\)-calculus ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ The bang calculus revisited ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Reasoning About Call-by-need by Means of Types ⋮ Exact bounds for acyclic higher-order recursion schemes

This page was built for publication: Non-idempotent intersection types and strong normalisation