A SEMANTICS FOR EVALUATION LOGIC

Article type: Research Article

Authors: Moggi, Eugenio

Affiliations: DISI, Univ. of Genova, viale Benedetto XV 3, 16132 Genova, Italy, moggi@disi.unige.it

Note: [] This work is supported by ESPRIT BRA 6811 (Categorical Logic In Computer Science II) and EC SCIENCE twinning ERBSC1*CT920795 (Progr. Lang. Semantics and Program Logics).

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.

DOI: 10.3233/FI-1995-22126

Journal: Fundamenta Informaticae, vol. 22, no. 1-2, pp. 117-152, 1995