Outline by Paper Sections
- Section 2:
- Syntax and semantics of source language
- Session type system
- Syntax and semantics of target language
- Translation from source to target (N.B.: in the original paper submission there was a small issue with order of argument evaluation)
- Observational refinement between source and target values
- Fairness-preserving refinement (generic)
- Section 3:
- Basic propositions and proof rules of linear BI
- Weakest-precondition rules for target language:
- Step-shift rules for source language
- Proof rules for STSs
- N.B.: the example for the small program in this section is not mechanized, since it is a consequence of our complete compiler correctness result
- Section 4:
- Extension 1: Linearity
- Extension 2: Stepping
- CMRA resources extended with step relations
- Modified definition of weakest-precondition with stepping of resources (last line).
- Step-shift modality
- Soundness
- Generic forms of lemma (versions in paper are instantiated for source language)
- Instantiated theorem for establishing refinement
- Section 5:
- Logical relation for values
- STS interpretation for channel protocol
- Derived proof rules for channel primitive implementations (N.B.: these proof scripts are redundant and not writen in good style)
- Compiler correctness theorem (N.B.: the proof uses classical axioms, hence "Print Assumption" command at end)
- Appendix B.1:
- Lifting logical relation from values to expressions
- Logical relation for values
- Lifting logical relation to open expressions
- Soundness of logical relation
- Fundamental theorem (N.B.: the reasoning about substitutions here could be cleaned up)
- Appendix B.2
Outline of Notable Files
- prelude: extended "Standard Library" by Robbert Krebbers, with modifications
- irelations.v -- definitions and general results about fair infinite executions of indexed transition systems
- algebra:
- cmra -- the algebraic structures representing "resources"
- upred -- model of propositions, basic BI proof rules
- sts -- STS CMRA instance
- program_logic:
- language -- generic definition of languages that can be reasoned about in Iris
- weakestpre -- definition of weakest precondition.
- pviewshifts -- view-shift modality
- pstepshifts -- step-shift modality
- adequacy -- generic adequacy theorems for finite executions
- adequacy_inf -- generic adequacy theorems for infinite executions
- refine_ectx_delay -- generic "source" thread resource monoid proof rules, refinement soundness theorem
- heap_lang: target language
- lang -- syntax and semantics
- lifting -- basic weakest-precondition proof rules ("big-footprint")
- heap -- small-footprint rules using fracitonal-heap CMRA
- proofmode -- tactic support
- refine -- step-shift rules for refinements from heap_lang
- refine_proofmode -- tactic support for refinements from heap_lang
- chan_lang: source language
- lang -- syntax and semantics
- simple_types -- simple session types
- refine -- big-footprint step-shift rules for refinements from chan_lang
- refine_heap -- small-footprint step-shift rules for refinements from chan_lang, using heap CMRA
- refine_heap_proofmode -- tactic support
- chan2heap: session typed language compiler and correctness result
- chan2heap -- translation from channel to heap languages
- refine_protocol -- derived proof rules for implementations of message passing primitives
- simple_reln -- logical relation
- Lifting logical relation from values to expressions
- Logical relation for values
- Lifting logical relation to open expressions
- Soundness of logical relation
- Fundamental theorem
- compiler_correctness -- statement and proof of correctness result.
- tests:
- heap_lang -- simple example refinements from heap_lang to heap_lang (loop hoisting, re-orderings reads/writes/forks).