From semantics to types: the case of the imperative \(\lambda\)-calculus

DOI10.1016/j.tcs.2023.114082arXiv2112.14053OpenAlexW4385075797MaRDI QIDQ6093581

Ugo de'Liguoro, Riccardo Treglia

Publication date: 7 September 2023

Published in: Theoretical Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

type assignment systemsfilter modelsstate monadimperative lambda calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Categorical semantics of formal languages (18C50) Combinatory logic and lambda calculus (03B40)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• Generic models for computational effects
• Discrete Lawvere theories and computational effects
• Type inference for polymorphic references
• Domain theory in logical form
• Functional programming languages and computer architecture. 5th ACM conference, Cambridge, MA, USA, August 26-30, 1991. Proceedings
• Full abstraction in the lazy lambda calculus
• A syntactic theory of sequential state
• The type and effect discipline
• A syntactic approach to type soundness
• Intersection type assignment systems
• Algebraic operations and generic effects
• The untyped computational \(\lambda \)-calculus and its intersection type discipline
• Intersection types and lambda models
• Programming languages and systems. 28th European symposium on programming, ESOP 2019, held as part of the European joint conferences on theory and practice of software, ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings
• Functors are Type Refinement Systems
• The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads
• Intersection types and computational effects
• A filter lambda model and the completeness of type assignment
• Not Enough Points Is Enough
• The Category-Theoretic Solution of Recursive Domain Equations
• Execution time of λ-terms via denotational semantics and intersection types
• A tale of intersection types
• The marriage of effects and monads
• A complete characterization of complete intersection-type preorders
• Reading, Writing and Relations
• Parametric effect monads and semantics of effect systems
• Recursive Domain Equations of Filter Models

This page was built for publication: From semantics to types: the case of the imperative \(\lambda\)-calculus