Retrofitting Purity with Comonads and Capabilities
- π€ Speaker: Vikraman Choudhury, Indiana University / Cambridge
- π Date & Time: Friday 24 May 2019, 14:00 - 15:00
- π Venue: FW26
Abstract
We present a call-by-value effectful lambda calculus with capabilities, with a comonad that filters out pure expressions. We give a categorical semantics for it and show the soundness of substitution. We give an equational theory for our calculus and prove soundness for it. Finally, we give a translation from the pure call-by-value lambda calculus to our calculus, and show that it preserves the equational theory.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- tcw57βs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)

Vikraman Choudhury, Indiana University / Cambridge
Friday 24 May 2019, 14:00-15:00