Abstract
This paper proposes an internal semantics for the modalities and evaluation predicate of Pitts' Evaluation Logic, and introduces several predicate calculi (ranging from Horn sequents to Higher Order Logic), which are sound and complete w.r.t. natural classes of models. It is shown (by examples) that many computational monads satisfy the additional properties required by the proposed semantics.
Get full access to this article
View all access options for this article.