Operational, Denotational and Logical Descriptions: A Case Study¹

Article type: Research Article

Authors: Egidi, Lavinia^a | Honsell, Furio^b | Ronchi Della Rocca, Simona^a

Affiliations: [a] Dipartimento di Informatica, Università degli Studi di Torino, Italy | [b] Dipartimento di Matematica e Informatica, Università degli Studi di Udine, Ilaly

Note: [1] Work partially supported by MURST 40% and 60% grants and EEC “Project Stimulation ST2J/0374/C(EDB): Lambda Calcul Type”.

Abstract: The functional fragment of Landin’s ISWIM as implemented by the SECD machine is the paradigm of the procedural kernel of many programming languages. We investigate and compare operational, denotational and logical descriptions of the ISWIM-SECD system. Our goal is to illustrate how to derive from each of these descriptions logical tools for resoning about termination and equivalence of programs. First we show the correctness and incompleteness of the canonical denotational semantics. Then we give a fully abstract quotient semantics using a notion of applicative bisimulation. We discuss next a finitary logical description of the denotational semantics. This takes the form of a call-by-value intersection type assignment system. Finally we study this type assignment system for its own sake and give a completeness result for it with respect to a natural notion of interpretation.

DOI: 10.3233/FI-1992-16205

Journal: Fundamenta Informaticae, vol. 16, no. 2, pp. 149-169, 1992