D.pure_program_logic.weakestpre

• Expression weakest preconditions.
  • Derived rules

D.pure_program_logic.lifting

• Lift operational semantics to expression weakest preconditions.

D.pure_program_logic.adequacy

• Adequacy of expression weakest preconditions, part of gDOT adequacy.

D.iris_extra.det_reduction

• Define when a language is deterministic and when an expression is safe.
  • LangDet defines when a language is deterministic.
  • Safety for an arbitrary Iris language.
  • For a deterministic language, we can give a simpler definition.
  • For a deterministic language, safe_gen and safe are equivalent.

D.iris_extra.cmra_prop_lift

• Utilities for lifting camera properties to iProp, used in swap_later_impl.v and persistence.v.

D.iris_extra.dlang

• Instantiate Iris for D* languages.
  • Define Iris ghost state used by gD<:/gDOT proofs.
  • Instance of irisGS enable using the expression weakest precondition; this instance.

D.iris_extra.iris_prelude

• Notation for functions in the Iris scope.
• Automation for Iris program logic.
• Setoid rewriting
  • Enable rewriting from f x to g x with f ≡ g.
• Tactics for manipulating and using Proper instances.
  • Variants of solve_proper and solve_contractive that are more effective
  • Our best solve_proper/solve_contractive extension for higher-order
  • Other solve_proper/solve_contractive extensions for higher-order

D.iris_extra.lty

• Formalize infrastructure for semantic types; not shown in the paper.
  • "Iris Persistent Predicates" iPPred.
  • OFE on iPPred.
  • Show iPPred forms a COFE.
  • "Logical TYpes": persistent Iris predicates over values.
• "Open Logical TYpes": persistent Iris predicates over environments and values.
  • Substitution over olty.
  • Constructors for language-independent semantic types, corresponding to

D.iris_extra.persistence

• Show all of Iris propositions are persistent when resources are idempotent (like in our case).
• Show that our actual resources satisfy CmraPersistent.

D.iris_extra.proofmode_extra

D.iris_extra.pupd

• "Persistent updates".

D.iris_extra.proofmode_pupd

• Automation for the "persistent update" modalities.

D.iris_extra.saved_interp_dep

• Iris saved predicates.

D.iris_extra.saved_interp_n

D.iris_extra.swap_later_impl

• Show proof rule Impl-▷.
  • Interface to Swap laws for any bi.
  • Implementation of swap laws for uniform predicates.
  • CmraSwappable Instances.

D.prelude

• "Prelude" with utilities available everywhere.
  • Miscellaneous utilities

D.asubst_intf

• Basic interfaces for D* languages (such as D<:, Dot).
  • ValueSig describes parameters that each D* language must implement.
  • This module type contains minimal infrastructure for D*-languages.

D.asubst_base

• Substitution lemmas for languages implementing ValuesSig.

D.proper

• Utilities for setoids.

D.succ_notation

• ssreflect postfix notation for the successor and predecessor functions.

D.numbers

D.tactics

• Some common Ltac utilities.

D.Dot.syn.syn

• gDOT syntax and operational semantics.
  • DOT syntax, with corresponding on-paper syntax in comments.
  • Substitution infrastructure.
• Auxiliary definitions for operational semantics.
  • Auxiliary definitions for operational semantics: primitives.
  • Auxiliary definitions for operational semantics: object lookup.
  • Evaluation context nodes.
  • Head-reduction e →ₕ e'.

D.Dot.syn.rules

• Lift DOT operational semantics into rules for the Iris program logic.

D.Dot.syn.path_repl

• Path substitution and replacement.
  • The path replacement judgment, as defined in the pDOT paper.

D.Dot.syn.path_repl_lemmas

• Show correctness of functional path substitution.

D.Dot.syn.lr_syn_aux

• Iris-free auxiliary utilities for our gDOT logical relation.

D.Dot.syn.drop_skips

• Show simulation between terms and skip-free terms.

D.Dot.syn.skeleton

• Define correspondence between terms which only differ in type members.
  • same_skel_tm is a simulation.

D.Dot.syn.core_stamping_defs

D.Dot.syn.traversals

D.Dot.lr.dlang_inst

• Instantiate Iris and dlang with our gDOT language.

D.Dot.lr.dot_lty

• Semantic domains for DOT logical relations.
  • A "coherent" logical type, containing all semantics of a type.
• Constructions on gDOT semantic types.
  • Semantic path substitution and replacement.

D.Dot.lr.path_wp

• gDOT's path weakest precondition path_wp.

D.Dot.lr.dot_semtypes

• Logical relation and semantic judgments.
  • Define fully semantic judgments. They accept arbitrary semantic types.
  • gDOT semantic types.

D.Dot.lr.unary_lr

• Logical relation and semantic judgments.
• Value interpretation of types (Fig. 9).
  • Binding lemmas about gDOT logical relations.
  • Show these typing judgments are equivalent to what we present in the paper.

D.Dot.lr.sem_unstamped_typing

• Unstamped semantic judgments, adequacy, and typing lemmas.
  • Adequacy of unstamped semantic typing (Theorem 5.4).

D.Dot.semtyp_lemmas.later_sub_sem

• When is a context weaker than another? Semantic version.
• Basic lemmas about s_ctx_sub.

D.Dot.semtyp_lemmas.binding_lr

• Binding-related semantic typing lemmas.

D.Dot.semtyp_lemmas.defs_lr

• Semantic lemmas for definition typing.
  • Prove object introduction for path typing, using Löb induction:
  • Derive object introduction for term typing.

D.Dot.semtyp_lemmas.dsub_lr

• Semantic lemmas for single-delay subtyping.

D.Dot.semtyp_lemmas.path_repl_lr

• Semantic lemmas on singleton types, path typing and path replacement.

D.Dot.semtyp_lemmas.prims_lr

• Semantic lemmas for typing of primitive expressions.
  • Unary operations
  • Binary operations

D.Dot.semtyp_lemmas.tproj_lr

• Semantic lemmas for Scala 2 type projections T#A.
  • Semantic proofs of typing lemmas for existentials.
  • Semantics of type projections.
  • Semantic proofs of typing lemmas for projections.
  • Rules for projecting members with matching bounds.

D.Dot.syntyp_lemmas.binding_lr_syn

• Binding-related semantic typing lemmas.

D.Dot.syntyp_lemmas.dsub_lr_syn

• Semantic lemmas for single-delay subtyping.

D.Dot.syntyp_lemmas.path_repl_lr_syn

• Semantic lemmas on singleton types, path typing and path replacement.

D.Dot.syntyp_lemmas.prims_lr_syn

• Semantic lemmas for typing of primitive expressions.

D.Dot.syntyp_lemmas.later_sub_syn

• When is a context weaker than another? Semantic version.
• Basic lemmas about ctx_sub.

D.Dot.typing.subtyping

• Judgments defining syntactic gDOT path- and sub- typing.

D.Dot.typing.type_eq

D.Dot.typing.typing

• Judgments defining syntactic gDOT definition and term typing.
  • Judgments for typing, subtyping, path and definition typing.
  • A few derived rules, and some automation to use them in examples.

D.Dot.typing.typing_aux_defs

• Auxiliary typing judgments and lemmas, shared between different variants of the typing judgment.
  • When is a context weaker than another? While we don't give complete
  • The T1 ≫ ▷ T2 judgment, used in the Γ1 ≫ ▷ Γ2 paper judgment.
  • The Γ1 ≫▷ Γ2 judgment from the paper.

D.Dot.fundamental

• Fundamental theorem and type safety for gDOT.
• Fundamental theorem 5.3.

D.Dot.examples.ex_utils

• Infrastructure for examples of DOT programs.
• NOTATIONS
  • Notation for object values.
• AUTOMATION

D.Dot.examples.hoas

D.Dot.examples.hoas_ex_utils

• Infrastructure for examples of DOT programs that uses HOAS.
• Infinite loops

D.Dot.examples.stamping.unstampedness_binding

D.Dot.examples.old_typing.old_subtyping

• Judgments defining the previous version of gDOT subtyping.

D.Dot.examples.old_typing.old_subtyping_derived_rules

• Manipulating laters, basics.
• Derived constructions.
• Manipulating laters, more.

D.Dot.examples.old_typing.old_unstamped_typing

• Judgments defining gDOT unstamped typing.
  • Judgments for typing, subtyping, path and definition typing.
  • A few derived rules, and some automation to use them in examples.

D.Dot.examples.old_typing.old_unstamped_typing_derived_rules

• Derived constructions.
• Manipulating laters, more.

D.Dot.examples.old_typing.old_unstamped_typing_to_typing

• Prove syntactic translation from old unstamped typing to typing.

D.Dot.examples.old_fundamental

• Old fundamental theorem and type safety for storeless gDOT and old unstamped gDOT.
  • Old fundamental theorem for storeless gDOT.

D.Dot.examples.sem.semtyp_lemmas.sub_lr

• Semantic lemmas for double-delay subtyping.
• Proper instances.

D.Dot.examples.sem.semtyp_lemmas.examples_lr

• Semantic lemmas not used by the fundamental theorem.

D.Dot.examples.sem.syntyp_lemmas.sub_lr_syn

• Semantic lemmas for double-delay subtyping.
  • Show this typing judgment is equivalent to the more direct definition.

D.Dot.examples.sem.syntyp_lemmas.examples_lr_syn

D.Dot.examples.sem.ex_iris_utils

• Infrastructure for examples of DOT programs that use Iris.

D.Dot.examples.sem.no_russell_paradox

• Russell's paradox does not affect guarded impredicative type members.

D.Dot.examples.sem.prim_boolean_option

• • Define interface for hoptionModV.
  • Implement hoptionModV.

D.Dot.examples.sem.storeless_typing

• Judgments defining gDOT "storeless" typing.
  • A few derived rules, and some automation to use them in examples.

D.Dot.examples.sem.storeless_typing_ex

D.Dot.examples.sem.storeless_typing_ex_utils

D.Dot.examples.sem.from_pdot_mutual_rec_sem

• Motivating example, semantic version.
  • Additional examples of client code, not mentioned in the paper.

D.Dot.examples.sem.small_sem_ex

• Exercise: Semantic typing for positive numbers (smallest example).
  • Example code.

D.Dot.examples.sem.positive_div

• Semantic typing for positive numbers and division.
  • Example code.

D.Dot.examples.syn.from_pdot_mutual_rec

• Motivating example, syntactic version.

D.Dot.examples.syn.list

• Encoding covariant lists.
  • Interface of the list module.
  • Implementation of the list module.
  • Auxiliary types, needed in derivations of typing judgments.
  • Lemmas for proof that hlistModV has type hlistModT.
  • Proof that hlistModV has type hlistModT.
  • Link lists with booleans.
  • Link lists with booleans and with a client using the list API.

D.Dot.examples.syn.old_unstamped_typing_ex

D.Dot.examples.syn.scala_lib

• • Infinite loops; typed using old unstamped typing.
• Booleans, Church-encoded.

D.Dot.examples.syn.syn_lemmas

• Free-variable lemmas for DOT.

D.Dot.hkdot.sem_kind

• Semantic Full Kind.

D.Dot.hkdot.sem_kind_dot

• Type members
  • Type members: derive special case for gDOT.
• Path application and substitution

D.Dot.hkdot.hkdot

• Prefixes: K for Kinding, KStp for kinded subtyping, Skd for subkinding.
• Subkinding
• Kinded subtyping.
• Kinding

D.DSub.syn.rules

D.DSub.syn.syn

D.DSub.syn.syn_lemmas

D.DSub.lr.ty_interp_subst_lemmas

• Binding lemmas about DSub* logical relations.

D.DSub.lr.unary_lr

D.DSub.lr.semtyp_lemmas

D.DSub.typing.obj_ident_typing

D.DSub.typing.storeless_typing

D.DSub.fundamental