Operational, denotational and logical descriptions: A case study. (English) Zbl 0762.68042

Egidi, Lavinia; Honsell, Furio; Ronchi Della Rocca, Simona

Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 16, No. 2, 149-169 (1992).

Summary: 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 reasoning 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.

MSC:

68Q55	Semantics in the theory of computing
68N15	Theory of programming languages

Keywords:

functional programming; operational semantics equivalence; SECD machine