ICFP 2021
Sun 22 - Sat 28 August 2021
Sun 22 Aug 2021 19:00 - 19:30 at HOPE - Session 2

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 defi ned 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 nondeterministic, non-confluent, and normal forms are not unique. However, when interested in returning a value (convergence), the only necessary monadic rule is beta , whose evaluation is deterministic. The proof relies on tools coming from a calculus inspired by linear logic.

Slides (HOPE-Slide.pdf)393KiB

Sun 22 Aug

Displayed time zone: Seoul change

18:00 - 19:30
Session 2HOPE at HOPE
18:00
30m
Talk
The Functional Machine Calculus
HOPE
Willem Heijltjes University of Bath
18:30
30m
Talk
Formalising Algebraic Effects with Non-Recoverable Failure
HOPE
Timotej Tomandl University of Kent, Dominic Orchard University of Kent, UK
Pre-print
19:00
30m
Talk
Computational calculus: bridging reduction and evaluation
HOPE
Claudia Faggian Université de Paris & CNRS, Giulio Guerrieri University of Bath, Riccardo Treglia Università di Torino
File Attached