Skip to Main content Skip to Navigation
Conference papers

Evaluation and convergence in the computational calculus

Abstract : In Moggi's computational calculus, reduction is the contextual closure of the rules obtained by orienting three monadic laws. In the literature, evaluation is usually defined as the closure under weak contexts (no reduction under binders): E = | let x := E in M. We show that, when considering all the monadic rules, weak reduction is non-deterministic, non-confluent, and normal forms are not unique. However, when interested in returning a value (convergence), the only necessary monadic rule is β , whose evaluation is deterministic.
Document type :
Conference papers
Complete list of metadata
Contributor : Isabelle Gouat Connect in order to contact the contributor
Submitted on : Friday, June 25, 2021 - 6:16:36 PM
Last modification on : Tuesday, September 28, 2021 - 5:16:00 PM
Long-term archiving on: : Sunday, September 26, 2021 - 10:33:53 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License


  • HAL Id : lirmm-03271490, version 1



Claudia Faggian, Giulio Guerrieri, Riccardo Treglia. Evaluation and convergence in the computational calculus. 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy. ⟨lirmm-03271490⟩



Record views


Files downloads