Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Sun 18 Aug 2019 13:40 - 14:30 at Aurora Borealis - Invited Talk and Metatheory Chair(s): Jeremy Gibbons

Categorical structure is a source of great guidance in Type-Directed Development, despite the fact that today’s advanced type systems do a relatively poor job of expressing it. Meanwhile, recent progress in typed languages for algebraic effects and handlers do a less than perfect job of capturing the coherences which handlers for effectful operations should respect. The problem, as ever, is equality, but Cubical Type Theory offers an opportunity to improve the situation, by changing the way in which coherence properties are captured and ensuring uniformity in the treatment of things and of the equations which relate things. Correspondingly, I will offer grounds for optimism.

Sun 18 Aug

tyde-2019-papers
13:40 - 14:50: TyDe 2019 - Invited Talk and Metatheory at Aurora Borealis
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford
tyde-2019-papers13:40 - 14:30
Talk
tyde-2019-papers14:30 - 14:50
Talk
Stefan MonnierUniversité de Montréal
Link to publication