A SEMANTICS FOR EVALUATION LOGIC
Eugenio Moggi · Fundamenta Informaticae · 1995
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