University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Retrofitting Purity with Comonads and Capabilities

Retrofitting Purity with Comonads and Capabilities

Download to your calendar using vCal

  • UserVikraman Choudhury, Indiana University / Cambridge
  • ClockFriday 24 May 2019, 14:00-15:00
  • HouseFW26.

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:

Note that ex-directory lists are not shown.

 

Β© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity