Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Sun 3 Sep 2017 11:00 - 11:30 at L3 - Modular Semantics

Given a programming language, can we give a monadic denotational semantics that is stable under language extension? Models containing only a single monad are not stable. Models based on type-and-effect systems, in which there is a monad for every set of operations in the language, are. Cartwright and Felleisen, and Wadler, conjectured such monadic semantics can be generated. We describe a new general method of constructing stable models from standard monadic models, based on factorizations of monad morphisms. We show that under certain conditions factorizations induce a monad for every set of operations, and explain why the conditions usually hold. We also describe preliminary work using fibrations for logical relations generated from these factorization systems for proving the correctness of the resulting model.

Talk proposal (hope17-proposal.pdf)156KiB

Sun 3 Sep

Displayed time zone: Belfast change

10:30 - 11:30
Modular SemanticsHOPE at L3
10:30
30m
Talk
Higher-order Programming is an Effect
HOPE
File Attached
11:00
30m
Talk
A monadic solution to the Cartwright-Felleisen-Wadler conjecture
HOPE
Ohad Kammar University of Oxford, UK, Dylan McDermott University of Cambridge
File Attached