Lectures onType Theory
Part 1
Part 1

Typed Computation and Proof

  1. 1Judgments, Derivations, and Operational SemanticsCore route
  2. 2Simple Types, Curry–Howard, Safety, and NormalizationCore route
  3. 3First-Order Proof Theory and Sequent CalculiCore route
  4. 4Hindley–Milner Type InferenceCore route
  5. 5Semi-Unification and Polymorphic RecursionOptional
  6. 6Dimension Types and Units of MeasureOptional
  7. 7Row Polymorphism and Extensible Records and VariantsCore route
  8. 8Type-Preserving Compilation of Polymorphic RecordsOptional
  9. 9System F, Impredicativity, and NormalizationCore route
  10. 10Relational Parametricity and Abstraction TheoremsCore route
  11. 11Type Operators, Kinds, and System F-omegaCore route
  12. 12Existential Types, Abstract Data, and Representation IndependenceCore route
  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 QuantificationCore route
  19. 19Algebraic Subtyping and Principal InferenceOptional
  20. 20Intersection, Union, and Semantic SubtypingCore route
  21. 21Disjoint Intersections, Merge Elaboration, and CoherenceOptional
  22. 22Refinement Types and Proof-Carrying ProgramsCore route
  23. 23Gradual Typing and the Dynamic BoundaryOptional
  24. 24Recursive Types, Domains, and General RecursionCore route
  25. 25Object Calculi and Recursive Object TypesCore route
  26. 26Corrected Inference for Simple ObjectsOptional
  27. 27OO Self Types, F-Bounds, and MatchingCore route
  28. 28Effects, Monads, CBPV, and Algebraic OperationsCore route
  29. 29Scoped Operations and Explicit SubstitutionOptional
  30. 30Higher-Order Algebraic Effects and Modular ElaborationOptional
  31. 31Effect Rows, Principal Type-and-Effect Inference, and HandlersCore route
  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 SystemsCore route
  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 SystemsCore route
  61. 61Logical Frameworks, Encodings, and AdequacyCore route
  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 AnalysisCore route
  69. 69Symbolic Execution, Path Conditions, and Concolic TestingOptional
  70. 70Information-Flow Type Systems and NoninterferenceOptional

Search the book

Type to search the local edition.