1. **Step-indexed Semantics (done)**

Define a step-indexed extrinsic semantics of the imperative object calculus.

1.1: Define a small-step semantics

1.2: Define the notion of safety

1.3: Define types and store typings

1.4! Define object types

1.5! Prove the typing lemmas

1.6! Enrich the type system with subtyping

1.7. Extend the type system to recursive types

1.8. Extend the type system to impredicative polymorphism

(all these steps were also performed for the functional object calculus)

2. **Axiomatic Semantics**

Define a programming logic for the imperative object calculus by “extending” the type system developed at 1.

2.1.a. Extend the type systems with FOL assertions about the store (Abadi, Benton)

2.1.b. Extend the type systems with dependent types and use a shallow embedding to HOL (HTT)

2.2. Construct a deduction system by finding appropriate deduction rules

2.3! Prove that the deduction system is sound

–> Here is where we need a semantic model again! Hard to tell whether we can reuse some of the work from 1.

2.4!? Extend the programming logic towards local reasoning about the store (separation logic)

2.5!? Extend the programming logic towards modular reasoning about abstract data structures (specification logic, idealized ML)

3. **Transformation Semantics**

Define the semantics of the imperative object calculus in terms of a monadic transformation to a well-researched language with a strong deduction system.

3.1 Chose an appropriate language and extend it in order to accommodate all features of the imperative object calculus

3.1.a. Idealized ML

3.1.a.1: Extend it to records and subtyping on record types

3.1.a.2: Define a term-level fixed-point operator at monadic types using recursion through the store

3.1.a.3. Find an appropriate recursion rule

3.1.a.4! Prove soundness of the recursion rule

3.1.b. Hoare Type Theory

3.1.b.1. Define records using dependent products and sums

3.1.b.2? Extend HTT to subtyping on record types

3.2: Define a monadic transformation from the object calculus to the chosen target language (Dieter)

3.3. Prove that the monadic translation is type preserving (Dieter)

3.4! Prove that the monadic translation in correct with respect to

3.4.a? The operational semantics of both languages

3.4.b? The observable/termination behavior (contextual equivalence like)

3.4.c? Something else

3.5!? Extend the monadic translation from types to specifications (requires at least having some specification at 2.)

**Legend**

1.2 — the second subgoal of goal one

1.b — the second alternative to solve goal one

: — probably easy

. — probably not very easy, nor very challenging

! — probably challenging

? — unclear how, unclear how hard, unclear if possible (disambiguate later)