Definitions

• pDOT Abstract Syntax and Type System
  • Abstract Syntax
  • Opening
  • Path Replacement
  • Free variables
  • Record and Inert Types
  • Typing Rules
  • Well-typed stores
  • Infrastructure

Binding

• Opening and Substitution Properties and Environment Reasoning
  • Substitution definitions
  • Simple Implications of Typing
  • Opening Lemmas
  • Variable Substitution Lemmas

Weakening

• Weakening Lemma

ExampleTactics

• Tactics and Notations used in Examples

SingletonTypeExample

• Singleton-Types Example

CompilerExample

• Compiler Example

ListExample

• List Example

Sequences

• Xavier Leroy's Sequences Library
  • Finite sequences of transitions
  • Infinite sequences of transitions
  • Determinism properties for functional transition relations.

RecordAndInertTypes

• Reasoning About Records and Inert Types

Replacement

• Path Replacement T[q/p,n]

Subenvironments

• Subenvironments G1 ⪯ G2

Narrowing

• Narrowing Lemma

PreciseFlow

• Precise Typing (Elimination Typing I)
  • Precise typing for values
  • Precise Flow for Paths

PreciseTyping

• Precise Typing (Elimination Typing II and III)
  • II-level Precise Typing
  • III-level Precise Typing
  • Wellformed paths and environments
  • Strengthening and Typing of Singleton Types
  • Replacement Composition

TightTyping

• Tight typing ⊢]

InvertibleTyping

• Invertible (Introduction-pq) Typing
  • Invertible typing of paths G ⊢## p: T
  • Invertible typing for values

ReplacementTyping

• Replacement (Introduction-qp) Typing
  • Replacement Typing for Paths
  • Replacement typing for values

GeneralToTight

• Converting General Typing To Tight Typing
  • Sel-<: Replacement
  • Sngl-<: Replacement
  • General to Tight ⊢ to ⊢#
  • Proof Recipe

Lookup

• Runtime Configuration Lookup of Paths

Substitution

• Substitution and Renaming
  • Substitution Lemma
  • Renaming

CanonicalForms

• Canonical Forms
  • Type preservation for path lookup
  • Looking up well-typed paths
  • Canonical Forms for Functions (Lemma 5.5)

Reduction

• Operational Semantics
  • Normal forms

Safety

• Type Soundness
  • Safety wrt Term Reduction ⟼
  • Safety wrt Path Lookup ⤳
  • Extended Safety