TODO.md

CompCertOE paper

• Polish Sec. 2

  • Make sure notations are consistent

  • Drop CompCertO's string diagrams? [yes]

  • Improve 2.4

  • Decide on figures

  • Tikz string diagrams

• Rewrite Sec. 3 [June 3rd]

  • Follow this outline [5/26]

    • Layered composition [5/19]

      • Description

      • Simulations

      • Double category

      • String diagrams

      • Companions and conjoints

    • Spatial composition [5/23]

      • Motivation

      • Adjoining state

      • Simulation conventions

      • Lenses

      • String diagrams

    • Memory separation

    • Encapsulation

    • Applications

      • ClightP

      • CAL

  • Other tasks

    • Tweak/redistribute Sec. 2.4

    • Explain (+) as fixpoint, approximated by (.)

    • Better treatment of companion / conjoint

      • Before encapsulation

      • Explain *_mem

    • Add summary of compositional structure

      • 3D string diagram

      • New treatment of active vs. passive

• ClightP improvements

  • Frame as an application

  • Use the simpler proof Clight(M)@m*

• Make sure examples thread nicely / are complete but not redundant [June 1st]

• Discuss more related work

  • CCR

  • Interaction trees

  • BIP? (Bensalem et al)

Unusedglob

• Attempt with existing CompCertO [5/19]

  • Figure out what breaks

  • Write down document

• New approach to Genv

  • Revert to upstream Globalenv.v

  • Add new constructor with Senv.t oracle

  • Fix what breaks in common code

  • Fix a simple pass to validate

• Update Unusedglob proof

  • Update any needed dependencies (reachability analysis?)

  • Simulation convention

    • Can injp/inj be made to fit?

  • Update proof