Paper: A Logic for Algebraic Effects (at LICS 2008)

Authors: Gordon D. Plotkin Matija Pretnar

Abstract

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 first-order 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 lambda calculus, and also, via definable modalities, Hennessy-Milner logic, and evaluation logic, though Hoare logic presents difficulties.

BibTeX

  @InProceedings{PlotkinPretnar-ALogicforAlgebraicE,
    author = 	 {Gordon D. Plotkin and Matija Pretnar},
    title = 	 {A Logic for Algebraic Effects},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {118--129},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }