Semantic evaluation; intersection types and complexity of simply typed lambda calculus

DOI10.4230/LIPICS.RTA.2012.323MaRDI QIDQ5111914zbMATH OpenOpenAlexFDO

Authors Kazushige Terui

Publication date 27 May 2020

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2012/3501/pdf/24.pdf

zbMATH Keywords

computational complexitydenotational semanticsintersection typessimply typed lambda-calculus

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Combinatory logic and lambda calculus (03B40) Semantics in the theory of computing (68Q55)

Recommendations

• Execution time of λ-terms via denotational semantics and intersection types
• Functional and Logic Programming
• The simple type theory of normalisation by evaluation
• Recognizability in the Simply Typed Lambda-Calculus
• Compositional characterisations of \(\lambda\)-terms using intersection types

Cited in

(14)

• Execution time of λ-terms via denotational semantics and intersection types
• scientific article; zbMATH DE number 7561616 (Why is no real title available?)
• Bounded combinatory logic and lower complexity
• The IO and OI hierarchies revisited
• scientific article; zbMATH DE number 7029315 (Why is no real title available?)
• Implicit computation complexity in higher-order programming languages
• Finitary semantics of linear logic and higher-order model-checking
• Implicit automata in typed -calculi I: aperiodicity in a non-commutative logic
• Syntactically and semantically regular languages of -terms coincide through logical relations
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• Lambda calculus with algebraic simplification for reduction parallelisation: extended study
• Completeness of intersection and union type assignment systems for call-by-value -models
• scientific article; zbMATH DE number 6163261 (Why is no real title available?)
• Functional programs as compressed data

This page was built for publication: Semantic evaluation; intersection types and complexity of simply typed lambda calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111914)