HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Introducing ⦇ λ ⦈, a λ-calculus for effectful computation

Jirka Maršík 1 Maxime Amblard 2 Philippe de Groote 2
2 SEMAGRAMME - Semantic Analysis of Natural Language
Inria Nancy - Grand Est, LORIA - NLPKD - Department of Natural Language Processing & Knowledge Discovery
Abstract : We present λ , a calculus with special constructions for dealing with effects and handlers. This is an extension of the simply-typed λ-calculus (STLC). We enrich STLC with a type for representing effectful computations alongside with operations to create and process values of this type. The calculus is motivated by natural language modelling, and especially semantic representation. Traditionally, the meaning of a sentence is calculated using λ-terms, but some semantic phenomena need more flexibility. In this article we introduce the calculus and show that the calculus respects the laws of algebraic structures and it enjoys strong normalisation. To do so, confluence is proven using the Combinatory Reduction Systems (CRSs) of Klop and termination using the Inductive Data Type Systems (IDTSs) of Blanqui.
Complete list of metadata

Contributor : Maxime Amblard Connect in order to contact the contributor
Submitted on : Friday, April 16, 2021 - 3:35:24 PM
Last modification on : Friday, April 1, 2022 - 3:57:43 AM
Long-term archiving on: : Saturday, July 17, 2021 - 6:56:46 PM


Files produced by the author(s)



Jirka Maršík, Maxime Amblard, Philippe de Groote. Introducing ⦇ λ ⦈, a λ-calculus for effectful computation. Theoretical Computer Science, Elsevier, 2021, 869, pp.108-155. ⟨10.1016/j.tcs.2021.02.038⟩. ⟨hal-03200474⟩



Record views


Files downloads