Operational, Denotational and Logical Descriptions: A Case Study1

Publisher Website
Google Scholar
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.

This publication has 0 references indexed in Scilit: