Library structures.Poset

• Partially ordered sets

Library structures.Lattice

• Completely distributive lattices
  • Definition
  • Properties of sup and inf
• Joins and meets with predicates
• Derived operations
  • Binary joins
  • Greatest element
  • Binary meets
  • Properties

Library structures.Completion

• Poset completions

Library structures.Category

• Categories
• Monoidal structure
• CDLat-enriched categories
• Sets and functions

Library structures.Monad

Library structures.Effects

• Effect signatures
  • Direct sum
  • Empty signature
• Interpretations

Library lattices.Downset

• Interface
• Construction
  • Partial order
  • Distributive lattice
  • Embedding
  • Simulator

Library lattices.Upset

• Interface
• Construction
  • Opposite order
  • Upsets

Library lattices.FCD

• Interface
• Specification
• Construction

Library lattices.LatticeProduct

Library lattices.AdjoinBot

• • Poset
  • Lattice structure
  • Adjunction

Library models.Sets

• Category of sets and functions
  • Core definitions
  • Endofunctors
  • Monoidal Structures
  • Overall definition
  • The terms for an effect signature E define a monad

Library models.Signature

• Signatures
  • Definition
  • Dependent type presentation
• Endofunctors
  • Simple terms
  • Examples
• Homomorphisms
  • Definition
  • Identity
  • Composition
  • Example
• Operations on signatures
  • Sum
  • Tensor
  • Composition
• Embeddings of Set
  • Covariant embedding

Library models.EffectSignatures

• Effect signatures
  • Definition
    • Basic definition
    • Dependent type presentation
    • Converting between the two forms
  • Applications
  • Homomorphisms
  • Compositional structure
  • Products
    • Products of arbitrary arity
    • Binary products
  • Coproducts
    • Coproducts of any arities
    • Binary coproducts
  • Terms over a signature
    • Definition
    • Substitutions
    • Variable renaming
    • Monadic multiplication
    • Applying homomorphisms to terms
  • Tensor product
  • Composition product
  • Putting everything together
• Interpretation in SET endofunctors
• Regular maps
  • Definition
  • Regular maps generalize signature homomorphisms
• Interpretation in SET monads

Library models.IntSpec

• Preliminaries
• Free interpretation
  • Monad
  • Interaction

Library models.Coherence

• Coherence spaces
  • Definition
  • Cliques
  • Ordering
  • DCPPO structure
    • Least element
    • Directed supremum
• Basic categorical structure
  • Linear maps
    • Definition
    • Properties
  • Identity and composition
  • Action on cliques
  • Linear isomorphisms
• Simple constructions
  • Output
  • Input
• Cartesian structure
  • Binary product
    • Definition
    • Universal property
  • Binary coproducts
    • Definition
    • Universal property
  • Terminal object
    • Definition
    • Universal property
• Tensor product
  • Definition
  • Functoriality
  • Unit
  • Negation
• Sequential constructions
  • Composition
  • Exponential
    • Comonad structure

Library models.DCPO

• Definitions for DCPOs
  • Partial orders
  • Directed-complete partial orders

Library models.IntStrat

• Preliminaries
• §2 COMPOSITIONAL SEMANTICS FOR VERIFICATION
  • §2.2 Effect Signatures
    • Definition 2.1 (Effect signature)
    • Signature homomorphisms
      • Definition
      • Compositional structure
  • §2.6 Combining Effect Signatures
    • Definition 2.9 (Sum of signatures)
    • Monoidal structure with respect to emor
      • Functoriality of fcomp
      • Left (λ) and right (ρ) unitors and their inverses
      • Associator (α) and its inverse
      • Triangle and pentagon identities
      • Braiding (γ)
      • Unit coherence property
      • Hexagon identity
      • The braiding is its own inverse
    • Duplication and projections
      • Terminal morphism
      • Left projection
      • Right projection
      • Diagonal morphism
      • Tupling
• §3 STRATEGY MODEL
  • §3.1 Strategies
    • Def 3.1 (Strategy)
    • Useful lemmas
    • Determinism
    • Residuals
    • Signature homomorphisms
      • Residuals
  • §3.2 Layered Composition
    • Def 3.4 (Layered Composition of Strategies)
    • Theorem 3.5 (Properties of Layered Composition)
    • Isomorphisms
    • Functoriality of emor_strat
  • §3.3 Flat Composition
    • Definition 3.6 (Flat composition of strategies)
    • Embedding signature homomorphisms preserves flat composition
    • Theorem 3.7 (Properties of flat composition)
    • Symmetric monoidal structure
      • Left unitor properties
      • Right unitor properties
      • Associator properties
      • Braiding is its own inverse
      • Duplication and projections
• §4 REFINEMENT CONVENTIONS
  • §4.2 Refinement Conventions
    • Definition 4.1 (Refinement convention)
    • Residual
    • Miscellaneous useful things
  • §4.3 Refinement Squares
    • Definition 4.2 (Refinement square)
    • Monotonicity properties
    • Determinism hints
    • Operational behavior
    • Preservation of joins and meets
    • Theorem 4.3 (Horizontal composition of refinement squares)
    • Definition 4.4 (Identity refinement convention)
    • Theorem 4.5 (Refinement ordering as refinement squares)
  • §4.4 Vertical Composition
    • Definition 4.7 (Vertical composition of refinement conventions)
    • Theorem 4.8 (Vertical composition of refinement squares)
    • Other properties of vertical composition
  • Signature homomorphisms
    • Definition
    • Useful lemmas
    • Functoriality
  • §4.5 Flat Composition
    • Definition 4.10 (Flat composition of refinement conventions)
    • Theorem 4.11 (Flat composition properties)
      • Functoriality of ⊕
      • Flat composition of refinement squares
    • Monoidal structure
• §5 SPATIAL COMPOSITION
  • §5.1 Explicit State
    • Tensor product of effect signatures
    • Tensor product of signature homomorphisms
      • Functoriality
      • Left unitor
      • Right unitor
      • Associator
      • Braiding
      • Coherence diagrams
    • Tensor product of strategies
      • Residuals
    • Tensor product of refinement conventions
      • Residuals
      • Preservation of sup and inf.
      • Functoriality vs vertical composition
    • Tensor product of refinement squares
  • §5.2 Passing State Through
  • §5.3 Transforming State
    • Bijections
      • Composition
      • Inverse
      • Product
      • Left unitor
      • Right unitor
      • Associator
      • Braiding
      • Triangle diagram
      • Pentagon diagram
      • Unit coherence for braiding
      • Hexagon
    • Lenses
      • Equivalence
      • Embedding bijections
      • Composition
      • Tensor product
      • Initial lens
      • Promoting a stateful lens to a strategy
      • Refinement conventions and refinement squares
    • §5.4 State Encapsulation
      • Encapsulation primitive
      • Companion and conjoint of a stateful lens
    • Spatial Composition
      • Definitions
      • Functoriality
      • Horizontal structural isomorphisms
      • Additional properties of embedded structural isomorphisms

Library models.LinCCAL

• Linearization-based Concurrent Certified Abstraction Layers
  • Concurrent object specifications
    • Definition
    • State-based representations
  • Implementation states
    • Environment steps
    • Commit steps
  • Correctness
    • Rechability predicate
    • Coinductive property
    • Proof method
  • Identity
  • Composition
    • Per-thread invariant
    • Global state invariant
    • Overall invariant
  • Certified abstraction layers form a category
• Example
  • Counter specification
  • Lock specification
  • Register specification
  • Horizontal composition (TODO: generalize)
  • Implementation

Library examples.CAL

• Preliminaries
• Effect signatures
  • Ring buffer
  • Bounded queue
• Layer implementation
• Layer interfaces
• Layer interfaces and implementations as morphisms
  • Keeping track of state
  • Properties
  • Rewriting tactic
  • Example
• Data refinement
  • Simulation relations as morphisms
  • Correctness of M_bq

Library interfaces.Category

• Introduction
• Category interface
  • Definition
  • Theory
    • Notations
    • Isomorphisms
    • Opposite category
  • Overall interface
• Basic instances
  • Trivial categories
  • Category of types and functions
  • Product category

Library interfaces.Functor

• Functors
  • Core definition
  • Additional properties
• Bifunctors
  • Definition
  • Properties
  • Bundled interface

Library interfaces.MonoidalCategory

• Monoidal structures
• Monoidal closure
• Cartesian monoidal structures
  • Definition
  • Consequences
    • Useful lemmas
    • Bifunctor structure
    • Monoidal structure
  • Cartesian category interface
• Monoidal functors

Library interfaces.ConcreteCategory

• Mathematical structures and enrichment
• Concrete categories
  • Definition
  • Theory
    • Objects
    • Morphisms
    • Composition
    • Derived constructions
  • Overall interface
• Basic instances
• Enrichment

Library interfaces.FunctorCategory

• Functor categories
• Functor composition
• Monoidal category of endofunctors under composition
• Monads
  • Monoid objects and homomorphisms
  • Compositional structure

Library interfaces.Limits

• Products
  • Category with all products
  • Derived cartesian structure
  • Preservation
• Coproducts
  • Category with all coproducts
• Limits in general
  • Specific types of limits