Logic in Computer Science, Symposium on (2008)

June 24, 2008 to June 27, 2008

ISSN: 1043-6871

ISBN: 978-0-7695-3183-0

pp: 118-129

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2008.45

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.

INDEX TERMS

algebraic operations, call-by-push-value, computational effects, computational lambda-calculus, program logics

CITATION

Matija Pretnar,
Gordon Plotkin,
"A Logic for Algebraic Effects",

*Logic in Computer Science, Symposium on*, vol. 00, no. , pp. 118-129, 2008, doi:10.1109/LICS.2008.45