Lectures onType Theory
Part 3
Part 3

Checking, Semantics, and Metatheory

  1. 110Trusted Kernels and Bidirectional CheckingCore route
  2. 111Canonicity, Normalization, and Decidable ConversionCore route
  3. 112Elaboration and UnificationCore route
  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 MatchingCore route
  13. 122Datatype Declaration Blocks and Strict PositivityCore route
  14. 123Recursive Function Groups and TerminationCore route
  15. 124Corecursive Definitions, Copatterns, and ProductivityCore route
  16. 125Elaborating Dependent Copattern DefinitionsCore route
  17. 126Erasure and Execution of Dependent DefinitionsCore route
  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 RepresentabilityCore route
  33. 142Adjunctions, Limits, and Locally Cartesian ClosureCore route
  34. 143Categorical Logic, Hyperdoctrines, and Internal LanguagesCore route
  35. 144Triposes, Toposes, and RealizabilityOptional
  36. 145Classical Realizability, Poles, and OrthogonalityOptional
  37. 146Algebraic Syntax, CwFs, and InitialityCore route
  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 TheoryCore route
  43. 152Groupoid and Path-Object Models of Intensional Type TheoryCore route
  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 UniversesCore route
  48. 157Games, Arenas, and StrategiesOptional
  49. 158Definability and Full Abstraction for PCFOptional
  50. 159Symmetric Monoidal Categories and Graphical Linear SemanticsCore route
  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 ParametricityCore route
  56. 165Sized Copattern Recursion and Mixed Induction–CoinductionOptional
  57. 166Parametric Large Sizes and Realizability ConsistencyOptional
  58. 167Internal Parametricity without an IntervalOptional

Search the book

Type to search the local edition.