semantics.base.overture

• Overture
  • Import ssreflect
  • Import setoid rewriting and tactics
  • Flags
  • Execute a tactic without introducing fresh assumptions
  • Path Types
  • Dependent Pairs
  • Predicates and relations
  • Indexed products
  • Mere propositions
  • Equivalence of types

semantics.base.meta

• Coq infrastructure
  • Turning type class failure into subgoals
  • Manually invoking unification / canonical structure inference

semantics.base.pext

• Propositional Extensionality

semantics.base.inhab

• Propositional Truncation / Squash Types
  • Definitions
  • Eliminators
  • Propositionality
  • Mere existence and surjectivity
  • Inhabitation elimination tactic
  • Bijective functions are equivalences

semantics.base.fext

• Functional Extensionality
  • Deriving functional extensionality from the existence of an interval
  • Extensionality for products
  • Extensionality Tactic
  • Propositions are closed under products
  • Pairs in bool -> X
  • Paths between Equivalences
  • Characterization of Maps out of Truncations

semantics.base.quotient

• Quotients
  • Relation Quotient Types
  • Characterization of maps out of quotients

semantics.base

semantics.ord.protype

• Pre-ordered Types
  • Operations
  • Setoid Rewriting
  • Induced preorder
  • Reverse preorder
  • Least upper and greatest lower bounds

semantics.ord.ordtype

• • Ordered Type
  • Operations
  • Induced order
  • Reverse order
  • Least upper and greatest lower bounds

semantics.ord.clat

• • Complete Lattices
  • Operations
  • Inf-closed predicates
  • Sup-closed predicates

semantics.ord.frame

• • Operations

semantics.ord.mono

• • Monotone functions
  • Laws

semantics.ord.adj

• Adjunctions
  • Adjunction type classes

semantics.ord.cont

• Continuous Functions

semantics.ord.prop

• • Order on propositions

semantics.ord.prod

• Order on Products
  • Order on binary products
  • Order on Dependent Functions
  • Order on functions

semantics.ord.mfun

• Order on Monotone Functions
  • Order on monotone functions
  • CLat Structure on monotone functions
  • Kripke Frames

semantics.ord.presheaf

• Presheafs / Lower Sets
  • Yoneda Embedding

semantics.ord.sheaf

• Sheafs
  • Covers
  • Basis
  • Sheafs over a basis
  • Order on Sheafs
  • Complete Lattics Structure on Sheafs
  • Frame Structure on Sheafs
  • Sheafification
  • Subcanonical Coverages
  • The canonical coverage on a proType
  • Every Frame is isomorphic to the frame of sheafs with its canonical basis.

semantics.ord

semantics.ars

• Abstract Reduction Systems

semantics.data.fintype

• • Finite Types

semantics.debruijn.syntax

• • Well-scoped untyped lambda terms.
  • Instantiation
  • Renaming as a special case of instantiation
  • Definitional laws
  • Identity law
  • Composition law

semantics.debruijn.reduction

• • One-Step Reduction

semantics.ccomega.sorts

• Universe Hierarchy

semantics.ccomega.syntax

• Syntax of CComega
  • Terms
  • Instantiation
  • Identity renaming law
  • Renaming as a special case of instantiation
  • Identity substitution law
  • Composition law

semantics.ccomega.reduction

• Reduction and Substitutivity in CComega
  • Single-step reduction
  • Many-Step Reduction
  • Conversion

semantics.ccomega.churchrosser

• Church-Rosser theorem for CComega
  • Reduction behaviour

semantics.ccomega.subtyping

• Cumulativity / Subtyping relation

semantics.ccomega.typing

• Typing
  • Type well-formedness

semantics.ccomega.contextmorphism

• Context Morphism Lemma

semantics.ccomega.subjectreduction

• Type soundness and subject reduction

semantics.f.types

• Syntax of System F Types
  • Instantiation
  • Renaming as a special case of instantiation
  • Identity law
  • Composition law
  • Simple Models

semantics.f.fcbvsyntax

• Syntax of fine-grained call-by-value System F terms
  • Instantiation
  • Identity renaming law
  • Renaming as a special case of instantiation
  • Identity substitution law
  • Composition law

semantics.f.fcbvreduction

• Big-step reduction relation for System Fcbv

semantics.f.weaknorm

• Weak normalization for System Fcbv

semantics.f.fsyntax

• Syntax of System F Terms
  • Instantiation
  • Identity renaming law
  • Renaming as a special case of instantiation
  • Identity substitution law
  • Composition law

semantics.f.fsemantics

• Semantics of System F

semantics.f.strongnorm

• Strong Normalization of System F
  • Logical Relation
  • Reducibility Candidates
  • Logical Relation
  • Logical relation on contexts
  • Fundamental theorem & Strong Normalisation

semantics.tower.tarski

• Order on fixed points
  • Fixed point operators

semantics.tower.associated_closure

• Inf-closed predicates and closure operators
  • The closure operator associated to an inf-closed predicate.
  • The equivalence between inf-closed predicates and closure operators.

semantics.tower.tower

• • The tower for f
  • The double induction principle
  • The companion for f

semantics.tower.parameterized

• Parameterized Tower Induction
  • Lemma 7.28: Parameterized Tower Induction principle
  • Lemma 7.29: Accumulation rule for the companion
  • Fact 7.30: Companion coinduction
  • Definition 7.31: Sound up-to functions
  • Lemma 7.32: Functions below the companion are sound

semantics.tower.llat

• • L-lattices and L-monotone functions
  • The L-lattice of complemented propositions
  • Products of L-lattices

semantics.tower.reals

• Interval Domain

semantics.tower.linear_tower

• • Constructive linearity and well-foundedness
  • Classical well-orderedness

semantics.tower.cocontinuous_tower

semantics.tower.gfp_companion

semantics.tower.ex_streams

• • Stream equality as a coinductive definition
  • Companion for stream equality
  • Cocontinuity

semantics.tower.ex_similarity

• • Labeled transition systems and similarity
  • Failure of cocontinuouity
  • Similarity at Type

semantics.tower.direct_induction

• Inf-closed co-induction and sup-closed induction
  • Directed and codirected families.
  • Inf-closed induction through closure operators.
  • Pataraia's fixed point theorem as an induction principle for greatest-fixed points.
  • Direct (co)induction

semantics.ccs.syntax

• Syntax of CCS with Recursive Processes
  • Processes
  • Instantiation
  • Unit Laws
  • Expressing map using bind
  • Associativity

semantics.ccs.semantics

• Semantics of CCS with Recursive Processes
  • Inversions

semantics.ccs.bisim

• Bisimilarity in CCS with Recursive Processes
  • Definition 8.1
  • Lemma 8.2
  • Definition 8.3
  • Monotonicity of the definitions
  • Fact 8.4
  • Lemma 8.5
  • Lemma 8.6: (Open) Relative Bisimilarity is an Equivalence Relation
  • Lemma 8.7
  • Congruence properties of open relative bisimilarity
  • Theorem 8.14: Open Relative Bisimilarity is a Congruence
  • Lemma 8.15: Open Relative Bisimilarity is Compatible with Instantiation

semantics.ccs.properties

• Properties of Strong Bisimilarity in CCS with Recursive Processes
  • Lemma 8.17
  • Corollary 8.18
  • Corollary 8.19

semantics.wp.prelim

• • Kleene's fixed point theorem
  • Continuous meet/suprema compatibility

semantics.wp.abstract

• • Fact 9.14
  • Fact 9.15
  • Definition 9.16
  • Lemma 9.17
  • Definition 9.18
  • Lemma 9.19
  • Definition 9.20
  • Lemma 9.21
  • Definition 9.23
  • Fact 9.24
  • Lemma 9.25
  • Lemma 9.26

semantics.wp.states

• Abstract States, Actions, and Guards

semantics.wp.gc

• Syntax of GCP
  • Syntax
  • Induction Principle
  • Decidable equality on terms
  • Specialized induction principle

semantics.wp.gcsemantics

• Semantics of GC
  • Axiomatic Semantics
  • Lemma 9.28
  • Lemma 9.29
  • Corollary 9.30
  • Lemma 9.31
  • Lemma 9.32

semantics.wp.ic

• Syntax of IC
  • Identity laws
  • Composition laws

semantics.wp.icsemantics

• • Small-step Semantics
  • Axiomatic semantics
  • Lemma 9.34
  • Lemma 9.35
  • Corollary 9.36
  • Lemma 9.37
  • Corollary 9.38
  • Lemma 9.39
  • Lemma 9.40
  • Lemma 9.41
  • Lemma 9.42
  • Lemma 9.43
  • Lemma 9.44
  • Corollary 9.45
  • Lemma 9.46

semantics.wp.compiler

• Compiler from GC to IC
  • Smart let
  • Lemma 9.49
  • Definition of the compiler
  • Theorem 9.50
  • Compiler correctness
  • Corollary 9.51