Lectures onType Theory
Part 2
Part 2

Dependent Calculi and Their Extensions

  1. 71The Rules of Dependent Type TheoryCore route
  2. 72Dependent Products, Sums, and UnitCore route
  3. 73Inductive TypesCore route
  4. 74Universes and Universe LevelsCore route
  5. 75Tarski Universes and DecodingOptional
  6. 76Universe Paradoxes and Hurkens's ConstructionOptional
  7. 77Identity TypesCore route
  8. 78Indexed Inductive Families and Dependent Pattern MatchingCore route
  9. 79Dependent Records and Primitive ProjectionsCore route
  10. 80Universes of Datatype Descriptions and Generic ProgramsCore route
  11. 81Containers, Polynomial Functors, and OrnamentsOptional
  12. 82Well-Founded RecursionCore route
  13. 83Size-Change TerminationOptional
  14. 84Mendler Recursion, Nested Datatypes, and Mixed VarianceOptional
  15. 85Coinduction, Copatterns, and BisimulationCore route
  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 ConstructionsCore route
  20. 90Extensional Type TheoryCore route
  21. 91Nuprl-Style Computational Type Theory and RealizabilityCore route
  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

Search the book

Type to search the local edition.