Towards verification of a denotational semantics of inheritance

Peter Mosses


Date: Wed, October 09, 2024
Time: 12:00
Room: Turing
Note: This is a rehearsal for a 25-minute talk to be given at JensFest, a SPLASH ’24 workshop


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’.

The paper in the proceedings1 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.

The talk is intended for a general audience; familiarity with Agda will not be assumed!

  1. A preprint of the paper will soon be made available. ↩

Previous: Pedro Abreu |
Next: |