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 <>
Submitted on : Friday, April 16, 2021 - 3:35:24 PM
Last modification on : Thursday, April 29, 2021 - 4:20:20 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-04-16

Please log in to resquest access to the document




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