Lectures onType Theory
Contents
Book map

Contents

Part 1

Typed Computation and Proof

  1. 1Judgments, Derivations, and Operational Semantics
  2. 2Simple Types, Curry–Howard, Safety, and Normalization
  3. 3First-Order Proof Theory and Sequent Calculi
  4. 4Hindley–Milner Type Inference
  5. 5Semi-Unification and Polymorphic RecursionOptional
  6. 6Dimension Types and Units of MeasureOptional
  7. 7Row Polymorphism and Extensible Records and Variants
  8. 8Type-Preserving Compilation of Polymorphic RecordsOptional
  9. 9System F, Impredicativity, and Normalization
  10. 10Relational Parametricity and Abstraction Theorems
  11. 11Type Operators, Kinds, and System F-omega
  12. 12Existential Types, Abstract Data, and Representation Independence
  13. 13Qualified Types, Type Classes, and Coherent Dictionary ElaborationOptional
  14. 14ML Modules: Abstraction, Functors, and SharingOptional
  15. 15MixML, Recursive Linking, and DefinednessOptional
  16. 16Modular Type Classes and Implicit ModulesOptional
  17. 17Typed Self-Representation in System F-omegaOptional
  18. 18Subtyping, Records, and Bounded Quantification
  19. 19Algebraic Subtyping and Principal InferenceOptional
  20. 20Intersection, Union, and Semantic Subtyping
  21. 21Disjoint Intersections, Merge Elaboration, and CoherenceOptional
  22. 22Refinement Types and Proof-Carrying Programs
  23. 23Gradual Typing and the Dynamic BoundaryOptional
  24. 24Recursive Types, Domains, and General Recursion
  25. 25Object Calculi and Recursive Object Types
  26. 26Corrected Inference for Simple ObjectsOptional
  27. 27OO Self Types, F-Bounds, and Matching
  28. 28Effects, Monads, CBPV, and Algebraic Operations
  29. 29Scoped Operations and Explicit SubstitutionOptional
  30. 30Higher-Order Algebraic Effects and Modular ElaborationOptional
  31. 31Effect Rows, Principal Type-and-Effect Inference, and Handlers
  32. 32Effect Capabilities and TunnellingOptional
  33. 33Modal Effect Types and Source-to-Met EncodingsOptional
  34. 34Lexical Effect Handlers and Direct CompilationOptional
  35. 35Control Operators and Classical ProofsOptional
  36. 36Linear and Affine Type Systems
  37. 37Evaluation-Strategy TranslationsOptional
  38. 38Ordered and Noncommutative Types and the Lambek CalculusOptional
  39. 39Polarization, Focusing, and Proof SearchOptional
  40. 40Proof Nets, Correctness Criteria, and Cut EliminationOptional
  41. 41Interaction Nets and Interaction CombinatorsOptional
  42. 42Optimal Sharing and Graph ReductionOptional
  43. 43Bunched Implications and Resource SemanticsOptional
  44. 44Separation Logic and Local ReasoningOptional
  45. 45Concurrent Separation Logic and Higher-Order Ghost StateOptional
  46. 46Ownership, Borrowing, and Affine Resource ProtocolsOptional
  47. 47Uniqueness Types and Destructive UpdateOptional
  48. 48Place Calculi, Partial Moves, and Field-Sensitive BorrowingOptional
  49. 49Mutable Value Semantics and inout AccessOptional
  50. 50Capability and Region Types for Typed Memory ManagementOptional
  51. 51Capture Types and Capture-Set PolymorphismOptional
  52. 52Typestate and State-Transition ProtocolsOptional
  53. 53Coeffects and Context-Dependent ComputationOptional
  54. 54Two Bases for Graded Types: Calculi and CorrespondenceOptional
  55. 55Temporal Types and Functional Reactive ProgrammingOptional
  56. 56Soft Linear Logic and Implicit ComplexityOptional
  57. 57Amortized Resource Analysis and Typed PotentialsOptional
  58. 58Binary Session Types and Typed ProtocolsOptional
  59. 59Multiparty and Asynchronous Session TypesOptional
  60. 60The Lambda Cube and Pure Type Systems
  61. 61Logical Frameworks, Encodings, and Adequacy
  62. 62Nominal Syntax, Support, and BindingOptional
  63. 63Contextual Modal Type Theory and BelugaOptional
  64. 64Dependent Nominal Type TheoryOptional
  65. 65Classical Simple Type Theory and HOLOptional
  66. 66System T and the Dialectica InterpretationOptional
  67. 67Bar Recursion, Choice, and Program ExtractionOptional
  68. 68Abstract Interpretation, Type Systems, and Verified Static Analysis
  69. 69Symbolic Execution, Path Conditions, and Concolic TestingOptional
  70. 70Information-Flow Type Systems and NoninterferenceOptional
Part 2

Dependent Calculi and Their Extensions

  1. 71The Rules of Dependent Type Theory
  2. 72Dependent Products, Sums, and Unit
  3. 73Inductive Types
  4. 74Universes and Universe Levels
  5. 75Tarski Universes and DecodingOptional
  6. 76Universe Paradoxes and Hurkens's ConstructionOptional
  7. 77Identity Types
  8. 78Indexed Inductive Families and Dependent Pattern Matching
  9. 79Dependent Records and Primitive Projections
  10. 80Universes of Datatype Descriptions and Generic Programs
  11. 81Containers, Polynomial Functors, and OrnamentsOptional
  12. 82Well-Founded Recursion
  13. 83Size-Change TerminationOptional
  14. 84Mendler Recursion, Nested Datatypes, and Mixed VarianceOptional
  15. 85Coinduction, Copatterns, and Bisimulation
  16. 86Recursive Effects and Interaction TreesOptional
  17. 87Compositional Linearizability and Modular Concurrent ObjectsOptional
  18. 88Possibility Reasoning and Linearizability Hoare LogicOptional
  19. 89The Calculus of Inductive Constructions
  20. 90Extensional Type Theory
  21. 91Nuprl-Style Computational Type Theory and Realizability
  22. 92Logic-Enriched Type Theory and Predicative MathematicsOptional
  23. 93Dependent Intersections and Same-Subject RefinementOptional
  24. 94Subject-Dependent Self TypesOptional
  25. 95Very Dependent FunctionsOptional
  26. 96CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost ReuseOptional
  27. 97The lambda-Pi-Calculus Modulo RewritingOptional
  28. 98Linear Dependent Type TheoryOptional
  29. 99Quantitative Dependent Type TheoryOptional
  30. 100Graded Modal Dependent Type TheoryOptional
  31. 101Graded Erasure and ExtractionOptional
  32. 102Dependent Session Types and Protocol-Indexed ProgrammingOptional
  33. 103Dependent Effects and Call-by-Push-ValueOptional
  34. 104Weakest Preconditions and Dijkstra MonadsOptional
  35. 105Partiality and General Recursion in Dependent Type TheoryOptional
  36. 106Dependent Subtyping, Refinement, and GradualityOptional
  37. 107Dependent Object Types: Type Members, Bad Bounds, and Recursive SelfOptional
  38. 108Fully Path-Dependent Types: Stable Paths, Singletons, and ModulesOptional
  39. 109Classical Dependent Type Theory and ControlOptional
Part 3

Checking, Semantics, and Metatheory

  1. 110Trusted Kernels and Bidirectional Checking
  2. 111Canonicity, Normalization, and Decidable Conversion
  3. 112Elaboration and Unification
  4. 113Efficient First-Order UnificationOptional
  5. 114Proof-Producing Tactics and the Kernel BoundaryOptional
  6. 115Rewriting, Simplification, and ReflectionOptional
  7. 116Typed Metaprogramming and Hygienic ElaborationOptional
  8. 117First-Class Universe Levels and Level PolymorphismOptional
  9. 118Sort Polymorphism and Stratified Type TheoryOptional
  10. 119Coercive Subtyping and Coherent Cast InsertionOptional
  11. 120Definitional Functoriality and Generic Type-Former ActionOptional
  12. 121Compiling Dependent Pattern Matching
  13. 122Datatype Declaration Blocks and Strict Positivity
  14. 123Recursive Function Groups and Termination
  15. 124Corecursive Definitions, Copatterns, and Productivity
  16. 125Elaborating Dependent Copattern Definitions
  17. 126Erasure and Execution of Dependent Definitions
  18. 127Partial Evaluation, Binding-Time Analysis, and the Futamura ProjectionsOptional
  19. 128Supercompilation, Driving, and GeneralizationOptional
  20. 129Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case StudyOptional
  21. 130Dependent Multi-Stage Type TheoryOptional
  22. 131Explicit Equality Evidence and System FCOptional
  23. 132Systems D and DC: A Dependent Haskell Core SpecificationOptional
  24. 133Typed Intermediate Languages and Certified Closure ConversionOptional
  25. 134A Certified Type-Preserving Compiler to AssemblyOptional
  26. 135Defunctionalization, Refunctionalization, and Abstract MachinesOptional
  27. 136Secure Compilation and Robust Property PreservationOptional
  28. 137Dependent Closure Conversion for the Calculus of ConstructionsOptional
  29. 138Dependency-Preserving A-Normal FormOptional
  30. 139Typed Functional Array Languages: Shapes, Uniqueness, and Parallel CompilationOptional
  31. 140Verified Metatheory and Realistic Trusted KernelsOptional
  32. 141Categories, Functors, and Representability
  33. 142Adjunctions, Limits, and Locally Cartesian Closure
  34. 143Categorical Logic, Hyperdoctrines, and Internal Languages
  35. 144Triposes, Toposes, and RealizabilityOptional
  36. 145Classical Realizability, Poles, and OrthogonalityOptional
  37. 146Algebraic Syntax, CwFs, and Initiality
  38. 147Generalized Algebraic TheoriesOptional
  39. 148Explicit-Substitution CalculiOptional
  40. 149Categorical Semantics of Scoped OperationsOptional
  41. 150Categorical Semantics of CoeffectsOptional
  42. 151Set and CwF Models of Type Theory
  43. 152Groupoid and Path-Object Models of Intensional Type Theory
  44. 153Setoid and PER Models of Type TheoryOptional
  45. 154Recursive Domain Semantics and Computational AdequacyOptional
  46. 155Dependent PER-Enriched Domain ModelsOptional
  47. 156Coherence and Local Universes
  48. 157Games, Arenas, and StrategiesOptional
  49. 158Definability and Full Abstraction for PCFOptional
  50. 159Symmetric Monoidal Categories and Graphical Linear Semantics
  51. 160Modal and Multimodal Dependent Type TheoryOptional
  52. 161Synthetic Phase Distinctions and Synthetic Tait ComputabilityOptional
  53. 162Guarded and Clocked Dependent Type TheoryOptional
  54. 163Synthetic Guarded Domain Theory and Step-Indexed SemanticsOptional
  55. 164Dependent Parametricity
  56. 165Sized Copattern Recursion and Mixed Induction–CoinductionOptional
  57. 166Parametric Large Sizes and Realizability ConsistencyOptional
  58. 167Internal Parametricity without an IntervalOptional
Part 4

Interaction, Probabilistic and Quantitative Semantics, and Quantum Computation

  1. 168Reversible Classical ComputationOptional
  2. 169Profunctors, Coends, and OpticsOptional
  3. 170Dependent Optics and Indexed Bidirectional StructureOptional
  4. 171Probabilistic Lambda Calculi and Program EquivalenceOptional
  5. 172Probability, Measure, Kernels, and Computable Sampling
  6. 173Computable Conditioning and Its LimitsOptional
  7. 174Continuous Probabilistic Languages and Quasi-Borel Semantics
  8. 175Inference as Semantics-Preserving Program TransformationOptional
  9. 176Probabilistic Program LogicsOptional
  10. 177Expected Cost and Probabilistic Resource AnalysisOptional
  11. 178Error Credits and Approximate Higher-Order ReasoningOptional
  12. 179Verified Compilation of Probabilistic ProgramsOptional
  13. 180Dependent Probability and Fibred MeasureOptional
  14. 181Differential Lambda Calculus and Resource Taylor ExpansionOptional
  15. 182Differentiable Semantics and Forward-Mode Automatic DifferentiationOptional
  16. 183Reverse-Mode Automatic Differentiation and Cotangent SemanticsOptional
  17. 184Quantum Lambda Calculi and Linear Quantum DataOptional
  18. 185Typed Quantum Circuits and Proto-Quipper-MOptional
  19. 186Linear-Dependent Quantum Programming and Proto-Quipper-DOptional
Part 5

Homotopy Type Theory and Univalent Mathematics

  1. 187Elementary Topology and Classical Homotopy
  2. 188Fibrations, Homotopy Groups, and Exact Sequences
  3. 189Types as ∞-Groupoids
  4. 190Simplicial Sets, Horns, and Kan Fibrations
  5. 191Model Categories and Simplicial Semantics of Type Theory
  6. 192A Homotopical Model of Univalence
  7. 193Univalence
  8. 194Proof and Program Transfer Modulo EquivalenceOptional
  9. 195Truncation Levels, Propositions, and Logic
  10. 196Connected Maps, Factorization, and Modalities
  11. 197Localization and Its Universal PropertyOptional
  12. 198Higher Inductive Types and Homotopy-Initiality
  13. 199QIIT and QWI Schemas, Elimination, and InitialityOptional
  14. 200Join Constructions and Connectivity
  15. 201Type-Theoretic Replacement and Univalent CompletionOptional
  16. 202Coverings, van Kampen, and the Fundamental Group
  17. 203Fiber Sequences and Suspension Methods
  18. 204Higher Groups, Spectra, and StabilizationOptional
  19. 205Eilenberg–Mac Lane SpacesOptional
  20. 206Ordinary CohomologyOptional
  21. 207Univalent Categories and Rezk Completion
  22. 208Adjunctions, Limits, and Colimits in Univalent Categories
  23. 209Simplicial Type Theory and Synthetic Infinity-CategoriesOptional
  24. 210Set-Level Mathematics in Univalent Foundations
  25. 211Completions and the Real Numbers
  26. 212Choice-Free HII Cauchy CompletionOptional
  27. 213Displayed Type Theory and Semisimplicial TypesOptional
Part 6

Equality, Computed

  1. 214Two-Level Type Theory and Strict Equality
  2. 215Observational Equality and Computational Extensionality
  3. 216Intrinsic Topology of the UniverseOptional
  4. 217Cubical Type Theory I: De Morgan Cubes
  5. 218Cubical Type Theory II: Cartesian Cubes and Computation
  6. 219Guarded Cubical Type TheoryOptional
  7. 220XTT and Computational Bishop SetsOptional
  8. 221Parametric Cubical Type Theory and HIT Free TheoremsOptional
  9. 222Higher Observational Type Theory: From Bridges to FibrancyTerminal
Reference

Appendices

  1. The Rules
  2. Solutions to Exercises
  3. Notation
  4. Signatures, Deltas, and Metatheorems
  5. Executable Supplements
  6. Programming Tutorials
  7. Bibliography

Search the book

Type to search the local edition.