Collapsing non-idempotent intersection types

DOI10.4230/LIPICS.CSL.2012.259MaRDI QIDQ4649551zbMATH OpenFDO

Authors Thomas Ehrhard

Publication date 22 November 2012

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2012.259

zbMATH Keywords

denotational semanticslambda-calculuslinear logic

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• The Scott model of linear logic is the extensional collapse of its relational model
• Non-idempotent intersection types and strong normalisation
• Intersection types for the resource control lambda calculi
• Linearization of the lambda-calculus and its relation with intersection type systems
• Quantitative types for the linear substitution calculus

Cited in

(32)

• The bang calculus revisited
• Taylor expansion, finiteness and strategies
• The spirit of node replication
• The Inhabitation Problem for Non-idempotent Intersection Types
• Revisiting call-by-value Böhm trees in light of their Taylor expansion
• The Scott model of linear logic is the extensional collapse of its relational model
• Relational graph models at work
• The bang calculus and the two Girard's translations
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• A Fresh Look at the λ-Calculus
• scientific article; zbMATH DE number 7204443 (Why is no real title available?)
• Tight typings and split bounds, fully developed
• Non-idempotent types for classical calculi in natural deduction style
• Essential and relational models
• On reduction and normalization in the computational core
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• The bang calculus revisited
• Node Replication: Theory And Practice
• Quantitative global memory
• Strong call-by-value and multi types
• Light genericity
• Fixpoint constructions in focused orthogonality models of linear logic
• Categorifying non-idempotent intersection types
• A profunctorial Scott semantics
• Semantic bounds and multi types, revisited
• Böhm and Taylor for all!
• Mirroring call-by-need, or values acting silly
• A quantitative approach to global state composition
• Genericity through stratification
• Hybrid intersection types for PCF
• Separating terms by means of multi types, coinductively
• Mirroring call-by-need, or values acting silly

This page was built for publication: Collapsing non-idempotent intersection types

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