Retrofitting Purity with Comonads and Capabilities

Add to your list(s) Download to your calendar using vCal

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

If you have a question about this talk, please contact Victor Gomes.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.