LFCS Seminar Tuesday 11th February: Alex Kavvos

Title: Adequacy for Algebraic Effects Revisited

 

Abstract

 

We prove an adequacy theorem for a general class of algebraic effects, including infinitary ones. Our theorem targets a version of call-by-push-value, so that it applies to many possible evaluation mechanisms, including call-by-value. Our calculus is given an operational semantics based on interaction trees, as well as a denotational semantics based on monad algebras. We prove our main adequacy result, viz. that denotational equivalence implies observational equivalence, using a traditional logical relations argument.