A Logic for Algebraic Effects

We present a logic for algebraic effects, based on the algebraic representation of computational effects by operations and equations. We begin with the a-calculus, a minimal calculus which separates values, effects, and computations and thereby canonises the order of evaluation. This is extended to obtain the logic, which is a classical firstorder multi-sorted logic with higher-order value and computation types, as in Levy’s call-by-push-value, a principle of induction over computations, a free algebra principle, and predicate fixed points. This logic embraces Moggi’s computational λ-calculus, and also, via definable modalities, Hennessy-Milner logic, and evaluation logic, though Hoare logic presents difficulties.

• Type: Conference
• Year: 2008
• Where: LICS
• Authors: Gordon D. Plotkin, Matija Pretnar
• Keywords: Computer Science, LICS 2008, Logic, Logic Embraces Moggi, firstorder Multi-sorted Logic