Jens Palsberg’s first research publication was an OOPSLA ‘89 paper, coauthored with William Cook. In that much-cited paper, the authors identify self-reference as a central feature of inheritance, and analyze it using fixed points. They then define both an operational and a denotational semantics of inheritance, and prove them equivalent. Their proof exploits an intermediate semantics, obtained by step-indexing the operational semantics – an early use of the so-called `fuel pattern’.

This paper presents an Agda formulation of the definitions and lemmas from the OOPSLA ’89 paper. The Agda proof assistant detected some minor issues when type-checking the definitions; after they had been fixed, Agda successfully checked all the steps in the proofs of the lemmas. The Agda definitions and proofs make the same assumptions as the OOPSLA ’89 paper about the existence of recursively defined Scott domains, and about the continuity of the defined functions.

Peter Mosses is professor emeritus at Swansea University, and currently visiting the Programming Languages Group at Delft University of Technology.

His research in semantics stretches back to Strachey’s Programming Research Group at Oxford in the early 1970s, where he contributed to the development of denotational semantics, and implemented SIS, a system for running programs based on their semantics. He was based at Aarhus University, Denmark, from 1976 to 2004.

The main focus of his research has been on pragmatic aspects of formal specifications – especially modularity. This led to the development of action semantics, MSOS (a modular variant of structural operational semantics) and component-based semantics. He is a principal investigator in the PLanCompS project (Programming Language Components and Specifications), He was also the initial coordinator of CoFI, the Common Framework Initiative, which designed the algebraic specification language CASL.