Library structures.Effects

• Effect signatures
  • Direct sum
  • Empty signature
• Interpretations

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.FreeCategories

• Free category generated by a quiver
  • Definition
• Related constructions
  • Embedding
  • Interpretation functor

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
  • Terms over a signature
    • Definition
    • Substitutions
    • Variable renaming
    • Monadic multiplication
    • Applying homomorphisms to terms
  • Binary coproducts
    • Initial object
    • Binary products
  • Tensor product
  • Composition product
  • Putting everything together
• Interpretation in SET endofunctors
• Regular maps
  • Definition
  • Coproducts
    • Initial object
    • Binary products
  • Putting everything together
  • Regular maps generalize signature homomorphisms
• Interpretation in SET monads

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.LinCCAL

• Linearization-based Concurrent Certified Abstraction Layers
  • Concurrent object specifications
    • Definition
    • State-based representations
    • Tensor product
  • Implementation states
    • Environment steps
    • Commit steps
  • Correctness
    • Rechability predicate
    • Liveness
    • Coinductive property
    • Proof method
  • Identity
  • Vertical composition
    • Per-thread invariant
    • Global state invariant
    • Overall invariant
  • Certified abstraction layers form a category
  • Horizontal composition
    • Tensor product of layer interfaces
    • Tensor product of layer implementations
    • Functoriality
    • Empty layer interface
    • Structural isomorphisms
    • Naturality properties
    • Coherence diagrams
  • Putting everything together
• Example
  • Counter specification
  • Lock specification
  • Register specification
  • Implementation
  • Why the liveness property is needed

Library interfaces.Category

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

Library interfaces.Functor

• Functors
  • Quiver homorphisms
  • Functors
  • Theory
    • Universal morphisms
  • Additional properties
• Bifunctors
  • Definition
  • Properties
  • Bundled interface

Library interfaces.MonoidalCategory

• Monoidal structures
  • Definition
    • Structural isomorphisms
    • Naturality properties
    • Pentagon identity
    • Triangle identity
  • Theory
    • Naturality of backward maps
    • Backward coherence diagrams
    • Overall interface
  • Monodal categories
• Monoidal closure
• Symmetric monoidal categories
  • Definition
    • Swap map
    • Naturality
    • Coherence diagrams
    • Swap is its own inverse
  • Theory
    • Basic properties
    • Backward coherence diagrams
• Cartesian monoidal structures
  • Definition
  • Consequences
    • Useful lemmas
    • Bifunctor structure
    • Monoidal structure
    • Compatibility of monoidal and cartesian structure
  • Cartesian category interface
• Cocartesian monoidal structures
  • Definition
  • Consequences
    • Useful lemmas
    • Bifunctor structure
    • Monoidal structure
    • Compatibility of monoidal and cocartesian structure
  • Cocartesian 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

Library interfaces.Adjunctions

• Adjoint functors
  • Definition
  • Properties
    • Universal morphisms
    • Natural bijection

Library interfaces.Monads

• Defining monads
  • Full interface
  • By the Kleisli extension operator
  • As functor with extra structure
• Derived theory
  • Rewriting version of the core properties
  • Inter-definition of the various constructions
  • Kleisli category
    • Definition
    • Adjunction between the base and Kleisli categories

Library structures.Posets

• Partially ordered sets
  • Unbundled definitions
    • Suprema
    • Infrema
  • As extra structure for sets

Library structures.Lattices

• 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.DCPOs

• Directed-complete partial orders
  • Directed sets
    • Definition
    • Basic instances
    • Image through a monotonic function
  • DCPOs
    • Properties of dsup
    • Least element
    • Binary case for dsup
  • Derived DCPOs
    • Binary products
    • Dependent products
  • Scott-continuous functions
    • Definition
    • Equational statement
    • Composition
  • Category of DCPOs and strict Scott-continuous functions
• Free DCPO
  • Definition
  • Monad stuff / map from Set
• Fixed point constructions
  • Overview
  • Kleene fixed point
    • Approximation sequence
    • Limit
    • Properties
  • Ordinal numbers
    • Definition
    • Ordering
    • Ascending chains
  • Tarsky-style fixed point
    • Specification
    • Construction step
    • Definition
    • Well-foundedness

Library structures.DCPOSLs

• Dcpo-lattices
  • Free dcpo
  • Free semilattice
  • Free dcpo-semilattice
    • Carrier set
    • Lattice structure
    • DCPO structure
  • Monad operations
• ITree interoperability