Skip to content

References — Chapter 6 · Type Systems & Type Checking

Every source this chapter cites, grouped by kind. Lessons cite entries inline as [KEY]; each entry says why and when to read it. Core reading marks the entries the chapter assumes you will open.

Foundational and research papers

  • [BOSW98] Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Making the Future Safe for the Past: Adding Genericity to the Java Programming Language. OOPSLA 1998, 183–200, 1998. doi:10.1145/286936.286957
    Why and when: GJ, the design Java 5 adopted: generics compiled by erasure with bridge methods and casts inserted by the compiler. Read §2–3 after Lesson 6.9's erasure section and find the checkcasts of the javap box in its translation scheme.
    Cited in: 09-implementing-generics

  • [BTCGS91] Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as Implicit Coercion. Information and Computation 93(1), 172–221, 1991. doi:10.1016/0890-5401(91)90055-7
    Why and when: The coercion semantics of subtyping: every derivation of S <: T denotes a conversion function, and coherence (all derivations give the same function) is the theorem to prove. Read the introduction after Lesson 6.3 §6 and Lesson 6.5's "subtyping vs coercion".
    Cited in: 03-syntax-directed-checking, 05-subtyping

  • [Car88] Luca Cardelli. A Semantics of Multiple Inheritance. Information and Computation 76(2–3), 138–164, 1988. doi:10.1016/0890-5401(88)90007-7
    Why and when: Where structural record subtyping (width and depth) and the contravariant function rule come from. Read the typing rules for records and functions after Lesson 6.5 §2.
    Cited in: 05-subtyping

  • [CR02] Cliff Click and John Rose. Fast Subtype Checking in the HotSpot JVM. Joint ACM-ISCOPE Conference on Java Grande (JGI 2002), 96–107, 2002. doi:10.1145/583810.583821
    Why and when: How a nominal subtype test (Algorithm 6.5.9) becomes one load and compare at run time: a display of primary superclasses at fixed depths plus a cached secondary-supers search. Read §2–3 after Lesson 6.5 §5.
    Cited in: 05-subtyping

  • [CW85] Luca Cardelli and Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism. ACM Computing Surveys 17(4), 471–523, 1985. doi:10.1145/6041.6042
    Why and when: The classic taxonomy of polymorphism (parametric, inclusion, overloading, coercion) that Lessons 6.3, 6.5 and 6.9 use to separate overloading and coercions from subtyping and generics. Read §1.3 (kinds of polymorphism) after Lesson 6.2 and §3 (subtyping) with Lesson 6.5.

  • [DK13] Jana Dunfield and Neelakantan R. Krishnaswami. Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism. ICFP 2013, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, 429–442, 2013. doi:10.1145/2500365.2500582
    Why and when: A complete bidirectional algorithm for System F-style higher-rank types with an ordered context of existential variables. Read §1–3 after Lesson 6.4 §6 for how bidirectional checking extends to polymorphism; the context-based algorithm is the bridge to Chapter 7.
    Cited in: 04-bidirectional-typing

  • [Gri17] Radu Grigore. Java Generics are Turing Complete. POPL 2017, 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 73–85, 2017. doi:10.1145/3009837.3009871
    Why and when: Subtyping with Java's wildcards can simulate a Turing machine, so a type checker that decides it may not terminate. Read the introduction after Lesson 6.4 §5: it is why local inference stays deliberately weak and why variance (Lesson 6.5) must be designed with care.
    Cited in: overview, 04-bidirectional-typing, 05-subtyping

  • [IPW01] Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A Minimal Core Calculus for Java and GJ. ACM Transactions on Programming Languages and Systems 23(3), 396–450, 2001. doi:10.1145/503502.503505
    Why and when: Nominal subtyping in a calculus small enough to prove sound on one page, with casts as the one place a well-typed program may fail. Read §2 after Lesson 6.5's nominal/structural section and compare its extends-based subtyping with Definition 6.5.2.
    Cited in: 02-classifying-type-systems, 05-subtyping, 09-implementing-generics

  • [IV02] Atsushi Igarashi and Mirko Viroli. On Variance-Based Subtyping for Parametric Types. ECOOP 2002, LNCS 2374, 441–469, 2002. doi:10.1007/3-540-47993-7_19
    Why and when: Use-site variance annotations on parametric types, the direct ancestor of Java wildcards. Read §2 after Lesson 6.5's variance section.
    Cited in: 05-subtyping

  • [JJKD18] Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the Foundations of the Rust Programming Language. Proceedings of the ACM on Programming Languages 2(POPL), Article 66, 2018. doi:10.1145/3158154
    Why and when: A semantic soundness proof for a core of Rust's ownership and borrowing, including libraries built on unsafe. Read §1–2 after Lesson 6.8 §4 for what "the borrow checker is sound" means and why it is not a syntactic progress-and-preservation proof.
    Cited in: 01-judgments-and-safety, 08-places-and-references

  • [KS01] Andrew Kennedy and Don Syme. Design and Implementation of Generics for the .NET Common Language Runtime. PLDI 2001, ACM SIGPLAN Conference on Programming Language Design and Implementation, 1–12, 2001. doi:10.1145/378795.378797
    Why and when: The alternative to erasure: reified generics with code shared across reference types and specialized at load time for value types. Read §3–4 after Lesson 6.9 §6.
    Cited in: 09-implementing-generics

  • [Mil78] Robin Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17(3), 348–375, 1978. doi:10.1016/0022-0000(78)90014-4
    Why and when: Core reading. The origin of "well-typed programs cannot go wrong": §3 defines a denotational semantics in which "wrong" is a value and proves that well-typed expressions never denote it. Read §1–3 after Lesson 6.1 §1 to see the semantic route to soundness that Wright and Felleisen later replaced by a syntactic one; the inference half (Algorithm W) is Chapter 7's.
    Cited in: 01-judgments-and-safety

  • [PT00] Benjamin C. Pierce and David N. Turner. Local Type Inference. ACM Transactions on Programming Languages and Systems 22(1), 1–44, 2000. doi:10.1145/345099.345100
    Why and when: Core reading. Bidirectional checking ("local type propagation") plus local synthesis of type arguments, the design behind Scala and the target typing of Java and C#. Read §1–3 after Lesson 6.4 §1: the rules of §3 are the checking/synthesis split of Figure 6.4.2; §4 infers type arguments of polymorphic applications locally.
    Cited in: overview, 04-bidirectional-typing

  • [ST06] Jeremy G. Siek and Walid Taha. Gradual Typing for Functional Languages. Scheme and Functional Programming Workshop 2006, 81–92, 2006. link
    Why and when: Core reading. The origin of gradual typing: the dynamic type ?, the consistency relation and compilation to a cast calculus. Read it after Lesson 6.7 §2: Definition 6.7.2 and Algorithm 6.7.4 are its consistency relation and cast insertion, for a smaller language.
    Cited in: overview, 07-gradual-typing

  • [SVCB15] Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined Criteria for Gradual Typing. SNAPL 2015, LIPIcs 32, 274–293, 2015. doi:10.4230/LIPIcs.SNAPL.2015.274
    Why and when: The gradual guarantee (static and dynamic) of Theorem 6.7.7, which the lab tests on its corpus. Read §4 after Lesson 6.7 §4.
    Cited in: overview, 07-gradual-typing

  • [TFGNVF16] Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. Is Sound Gradual Typing Dead?. POPL 2016, 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 456–468, 2016. doi:10.1145/2837614.2837630
    Why and when: The performance lattice method and its sobering result for Typed Racket: some partially typed configurations run orders of magnitude slower than untyped ones. Read §2 and §5 after Lesson 6.7 §5; it is the source of the whole-program cost in the lesson's §5 and §8.
    Cited in: overview, 02-classifying-type-systems, 07-gradual-typing

  • [THEAG04] Mads Torgersen, Christian Plesner Hansen, Erik Ernst, Peter von der Ahé, Gilad Bracha, and Neal Gafter. Adding Wildcards to the Java Programming Language. SAC 2004, ACM Symposium on Applied Computing, 1289–1296, 2004. doi:10.1145/967900.968162
    Why and when: The design of ? extends / ? super and wildcard capture as it shipped in Java 5. Read it after the javac box of Lesson 6.5; the "CAP#1" in that output is its capture conversion.
    Cited in: 05-subtyping

  • [THF08] Sam Tobin-Hochstadt and Matthias Felleisen. The Design and Implementation of Typed Scheme. POPL 2008, 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 395–406, 2008. doi:10.1145/1328438.1328486
    Why and when: Occurrence typing: the type of a variable depends on the predicates that guard its occurrence. Read §3 (the formal system with latent predicates) after Lesson 6.6 §2.
    Cited in: 06-flow-sensitive-typing

  • [THF10] Sam Tobin-Hochstadt and Matthias Felleisen. Logical Types for Untyped Languages. ICFP 2010, 15th ACM SIGPLAN International Conference on Functional Programming, 117–128, 2010. doi:10.1145/1863543.1863561
    Why and when: Occurrence typing recast with propositions: every expression carries "then" and "else" propositions, combined by and/or/not exactly as Algorithm 6.6.3 combines the (true, false) states. Read §3–4 after Lesson 6.6 §4.
    Cited in: 06-flow-sensitive-typing

  • [WB89] Philip Wadler and Stephen Blott. How to Make Ad-hoc Polymorphism Less Ad Hoc. POPL 1989, 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 60–76, 1989. doi:10.1145/75277.75283
    Why and when: Type classes and their translation to dictionary passing: every class constraint becomes an extra argument holding the methods. Read §1–4 after Lesson 6.9 §2; the GHC Core in the lesson's box is this translation.
    Cited in: overview, 09-implementing-generics

  • [WF09] Philip Wadler and Robert Bruce Findler. Well-Typed Programs Can't Be Blamed. ESOP 2009, LNCS 5502, 1–16, 2009. doi:10.1007/978-3-642-00590-9_1
    Why and when: The blame calculus: casts carry labels with polarity, and the Blame Theorem says a cast failure is never the fault of the more precisely typed side. Read §2–3 after Lesson 6.7 §4 (Theorem 6.7.8) and compare its positive/negative blame with the lab's single labels.
    Cited in: overview, 07-gradual-typing

  • [WF94] Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Information and Computation 115(1), 38–94, 1994. doi:10.1006/inco.1994.1093
    Why and when: Core reading. The progress-and-preservation ("subject reduction") method of Lesson 6.1 §4, applied to ML-like languages with references and exceptions. Read §1–4 after Corollary 6.1.17; §5 shows why the method scales where the denotational proof of [Mil78] does not.
    Cited in: overview, 01-judgments-and-safety

Textbooks and monographs

  • [ALSU07] Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools, 2nd ed.. Addison-Wesley, 2007. Read: §6.3 (types and declarations), §6.5 (type checking: §6.5.1 rules, §6.5.2 conversions and widening, §6.5.3 overloading).
    Why and when: The compiler-writer's view of syntax-directed checking and conversions, with the widening hierarchy that Definition 6.3.4 formalizes. Read §6.5 alongside Lesson 6.3.
    Cited in: 03-syntax-directed-checking

  • [Pes24] Slava Pestov. Compiling Swift Generics. The Swift Project (swiftlang/swift, docs/Generics; PDF at download.swift.org), 2024. Read: Ch. 1 (introduction: generic calling convention, type metadata and witness tables), Ch. 7 (conformances and their witness tables).
    Why and when: The Swift compiler's own book on generics: dictionary passing through witness tables plus type metadata, and when the optimizer specializes instead. Read Ch. 1 after Lesson 6.9 §2.
    Cited in: 09-implementing-generics

  • [PFPL] Robert Harper. Practical Foundations for Programming Languages, 2nd ed.. Cambridge University Press, 2016. Read: Ch. 2–3 (inductive and hypothetical judgments), Ch. 4 (statics), Ch. 5 (dynamics), Ch. 6 (type safety), Ch. 22 (dynamic typing), Ch. 23 (hybrid typing), Ch. 24 (structural subtyping).
    Why and when: A more rigorous treatment of judgments, rule induction and safety than [TAPL]; Ch. 22–23 are the principled view of "dynamic typing as static typing with one type" behind Lessons 6.2 and 6.7. Read Ch. 4–6 if Lesson 6.1's proofs feel too compressed.
    Cited in: 01-judgments-and-safety, 02-classifying-type-systems

  • [Str94] Bjarne Stroustrup. The Design and Evolution of C++. Addison-Wesley, 1994. Read: §11.2 (overload resolution: the rules and their rationale), Ch. 15 (templates and their instantiation).
    Why and when: Why C++ overload resolution ranks conversions the way it does, and why templates were designed for compile-time instantiation (monomorphization). Read §11.2 with Lesson 6.3 and Ch. 15 with Lesson 6.9.
    Cited in: 03-syntax-directed-checking, 09-implementing-generics

  • [TAPL] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Read: Ch. 8 (typed arithmetic expressions: §8.3 safety = progress + preservation), Ch. 9 (simply typed lambda calculus: §9.3 properties, §9.4 Curry–Howard), Ch. 11 (simple extensions: records, let, ascription), Ch. 15 (subtyping), Ch. 16 (metatheory of subtyping: algorithmic subtyping, §16.1–16.3).
    Why and when: Core reading. The textbook this chapter's formal lessons follow. Read Ch. 8–9 with Lesson 6.1 (the arithmetic language of the progress-preservation drill is Ch. 8's), and Ch. 15–16 with Lesson 6.5 (Theorem 6.5.13 is the soundness and completeness result of §16.1 there).
    Cited in: overview, 01-judgments-and-safety, 05-subtyping

Surveys and tutorials

  • [Car96] Luca Cardelli. Type Systems. CRC Handbook of Computer Science and Engineering, ch. 103 (A. B. Tucker, ed.), CRC Press, 1996. link
    Why and when: Core reading. The best short survey of the whole chapter: judgments and rules (§3), type safety and the trapped/untrapped errors behind "strong" and "weak" typing (§1), subtyping (§6) and equivalence (§8). Read §1–3 before Lesson 6.1 and §1 again with Lesson 6.2, whose definitions follow it.
    Cited in: 01-judgments-and-safety, 02-classifying-type-systems

  • [DK21] Jana Dunfield and Neel Krishnaswami. Bidirectional Typing. ACM Computing Surveys 54(5), Article 98, 2021. doi:10.1145/3450952
    Why and when: Core reading. The survey Lesson 6.4 follows: mode-correctness, the Pfenning recipe (introduction forms check, elimination forms synthesize), annotatability and the subsumption rule. Read §2–4 alongside Lesson 6.4 §2–4; §7 surveys variants (spines, polarized systems).
    Cited in: overview, 04-bidirectional-typing

Source code (pinned versions)

  • [CLANG-ExprClass] Clang's value categories (lvalue, xvalue, prvalue) — clang/lib/AST/ExprClassification.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: ClassifyImpl, Expr::isModifiableLvalue.
    Why and when: One function computes the category of every C/C++ expression: the "place vs value" judgment of Definition 6.8.1. Read after Lesson 6.8 §2.
    Cited in: 08-places-and-references

  • [CLANG-SemaChecking] Clang's -Wconversion family of warnings — clang/lib/Sema/SemaChecking.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: CheckImplicitConversion, DiagnoseImpCast.
    Why and when: The heuristics behind -Wconversion, -Wsign-conversion and the literal-conversion warnings of Lesson 6.3's box: the conversions are legal C; the warnings are a separate analysis of value ranges.
    Cited in: 02-classifying-type-systems, 03-syntax-directed-checking

  • [CLANG-SemaExpr] Clang's expression checking (usual arithmetic conversions, assignment, l-values) — clang/lib/Sema/SemaExpr.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: Sema::UsualArithmeticConversions, Sema::CheckAssignmentConstraints, CheckForModifiableLvalue.
    Why and when: The syntax-directed checker of Lesson 6.3 in production: UsualArithmeticConversions implements C11 §6.3.1.8 (Algorithm 6.3.6), CheckAssignmentConstraints the "can this be assigned" relation, and CheckForModifiableLvalue the l-value errors of Lesson 6.8's box.
    Cited in: 01-judgments-and-safety, 03-syntax-directed-checking

  • [CLANG-SemaExprCXX] Clang's insertion of implicit conversions — clang/lib/Sema/SemaExprCXX.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: Sema::PerformImplicitConversion.
    Why and when: Where a chosen implicit conversion sequence becomes ImplicitCastExpr nodes in the AST, the elaboration step of Lesson 6.3 §2. Read after the AST-dump box of Lesson 6.1.
    Cited in: 03-syntax-directed-checking

  • [CLANG-SemaOverload] Clang's overload resolution — clang/lib/Sema/SemaOverload.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: OverloadCandidateSet::BestViableFunction, isBetterOverloadCandidate, CompareStandardConversionSequences, IsIntegralPromotion.
    Why and when: Conversion ranking (exact match, promotion, conversion) in CompareStandardConversionSequences and the best-viable-function tournament of Algorithm 6.3.8. Read after Lesson 6.3 §7; the ambiguity notes in the lesson's box come from here.
    Cited in: 03-syntax-directed-checking

  • [CLANG-TemplateInst] Clang's template instantiation (monomorphization) — clang/lib/Sema/SemaTemplateInstantiateDecl.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: Sema::InstantiateFunctionDefinition.
    Why and when: Where biggest<int> of Lesson 6.9's box is produced: the template's body is re-checked with the type arguments substituted. Read after Lesson 6.9 §7.
    Cited in: 09-implementing-generics

  • [GHC-Specialise] GHC's specialiser (dictionary passing turned into monomorphization) — compiler/GHC/Core/Opt/Specialise.hs in ghc/ghc at ghc-9.4.7-release. Symbols: specProgram.
    Why and when: The optimization that removes dictionary arguments by cloning overloaded functions at the types they are used at: Lesson 6.9 §6's hybrid. Read the long comment at the top after the GHC box.
    Cited in: 09-implementing-generics

  • [JAVAC-Attr] javac's attribution (type checking) of expressions — src/jdk.compiler/share/classes/com/sun/tools/javac/comp/Attr.java in openjdk/jdk at jdk-21+35. Symbols: Attr.ResultInfo, Attr.visitBinary, Attr.visitLambda.
    Why and when: javac threads an expected type (ResultInfo.pt) through attribution: syntax-directed for most expressions, target-typed for lambdas and generic methods (Lesson 6.4 §7). Read visitBinary for Lesson 6.3 and visitLambda for Lesson 6.4.
    Cited in: 03-syntax-directed-checking, 04-bidirectional-typing

  • [JAVAC-TransTypes] javac's erasure pass (casts and bridges) — src/jdk.compiler/share/classes/com/sun/tools/javac/comp/TransTypes.java in openjdk/jdk at jdk-21+35. Symbols: TransTypes.retype, TransTypes.coerce.
    Why and when: Where the checkcast instructions of Lesson 6.9's javap box are inserted: retype erases and coerce adds the cast back where the erased type is too general.
    Cited in: 09-implementing-generics

  • [JAVAC-Types] javac's subtyping, wildcard containment and erasure — src/jdk.compiler/share/classes/com/sun/tools/javac/code/Types.java in openjdk/jdk at jdk-21+35. Symbols: Types.isSubtype, Types.containsType, Types.erasure.
    Why and when: Nominal subtyping with generics: containsType decides ? extends/? super containment (use-site variance, Lesson 6.5) and erasure computes the erased types of Lesson 6.9.
    Cited in: 02-classifying-type-systems, 05-subtyping

  • [MYPY-Checker] mypy's narrowing by isinstance and is None — mypy/checker.py in python/mypy at v1.19.1. Symbols: find_isinstance_check, conditional_types.
    Why and when: Occurrence typing for Python: find_isinstance_check maps a condition to the (if, else) type maps of Definition 6.6.2. Read after the mypy box of Lesson 6.6.
    Cited in: 02-classifying-type-systems, 06-flow-sensitive-typing

  • [MYPY-Subtypes] mypy's subtype check and the Any type — mypy/subtypes.py in python/mypy at v1.19.1. Symbols: _is_subtype, SubtypeVisitor.visit_any.
    Why and when: Gradual typing in mypy: _is_subtype returns true when the right side is Any, and visit_any when the left side is (unless a proper subtype is asked for) — consistency folded into subtyping, with no cast inserted. Read after Lesson 6.7's mypy box.
    Cited in: 07-gradual-typing

  • [RUSTC-Borrowck] rustc's borrow checker, phase 1 (loans in scope as dataflow) — compiler/rustc_borrowck/src/dataflow.rs in rust-lang/rust at 1.94.1. Symbols: Borrows, kill_loans_out_of_scope_at_location.
    Why and when: Core reading. The forward gen/kill dataflow of Algorithm 6.8.8 on MIR: a loan is generated at its borrow and killed where its region ends. Read after Lesson 6.8 §2, then lib.rs (mir_borrowck) and region_infer/mod.rs (RegionInferenceContext::solve) for the regions themselves.
    Cited in: 08-places-and-references

  • [RUSTC-Closure] rustc's closure checking with an expected signature — compiler/rustc_hir_typeck/src/closure.rs in rust-lang/rust at 1.94.1. Symbols: check_expr_closure, deduce_closure_signature.
    Why and when: Why apply(|x| x + 1) needs no annotation: deduce_closure_signature reads the parameter types from the expected type. Read after the rustc box of Lesson 6.4.
    Cited in: 04-bidirectional-typing

  • [RUSTC-Coercion] rustc's coercions (the only implicit conversions in Rust) — compiler/rustc_hir_typeck/src/coercion.rs in rust-lang/rust at 1.94.1. Symbols: Coerce, Coerce::coerce_unsized.
    Why and when: Rust has no numeric promotion but does coerce references (auto-deref, unsizing, &mut to &) at "coercion sites", which are exactly the checking positions of Lesson 6.4. Read after Lesson 6.3 §7.
    Cited in: 03-syntax-directed-checking

  • [RUSTC-Mono] rustc's monomorphization collector — compiler/rustc_monomorphize/src/collector.rs in rust-lang/rust at 1.94.1. Symbols: collect_crate_mono_items, MonoItem.
    Why and when: The worklist of Algorithm 6.9.2: starting from roots, every instantiated generic function reachable from them becomes a MonoItem. Read after Lesson 6.9 §3.
    Cited in: 09-implementing-generics

  • [RUSTC-Typeck] rustc's expected types (the checking mode of its bidirectional checker) — compiler/rustc_hir_typeck/src/expectation.rs in rust-lang/rust at 1.94.1. Symbols: Expectation, Expectation::only_has_type.
    Why and when: Core reading. Expectation::ExpectHasType is the ⇐ of Lesson 6.4; check_expr_with_expectation in expr.rs next to it is the single entry point that switches modes. Read after Lesson 6.4 §7 and connect the "expected due to this" notes of the box to it.
    Cited in: 01-judgments-and-safety, 04-bidirectional-typing

  • [RUSTC-Variance] rustc's variance inference for type and lifetime parameters — compiler/rustc_hir_analysis/src/variance/mod.rs in rust-lang/rust at 1.94.1. Symbols: variances_of, crate_variances.
    Why and when: Rust infers declaration-site variance from how a parameter is used in the type's fields (a fixed point over the crate), instead of asking for annotations as Kotlin and Scala do. Read after Lesson 6.5's variance section.
    Cited in: 05-subtyping

  • [SWIFT-Exclusivity] Swift's static enforcement of exclusive access (on SIL) — lib/SILOptimizer/Mandatory/DiagnoseStaticExclusivity.cpp in swiftlang/swift at swift-6.1-RELEASE. Symbols: checkStaticExclusivity, diagnoseExclusivityViolation.
    Why and when: A dataflow over begin_access/end_access markers that reports overlapping accesses at compile time; AccessEnforcementSelection.cpp next to it decides which accesses need dynamic checks. Read after Lesson 6.8's exclusivity section.
    Cited in: 08-places-and-references

  • [SWIFT-GenProto] Swift's witness-table emission — lib/IRGen/GenProto.cpp in swiftlang/swift at swift-6.1-RELEASE. Symbols: FragileWitnessTableBuilder, emitSILWitnessTable.
    Why and when: How a protocol conformance becomes a table of function pointers passed to generic code (Lesson 6.9 §2); lib/SILOptimizer/Transforms/GenericSpecializer.cpp is the optimizer's monomorphizing counterpart.
    Cited in: 09-implementing-generics

  • [TSC-Checker] The TypeScript checker (narrowing, structural assignability, contextual typing) — src/compiler/checker.ts in microsoft/TypeScript at v5.9.3. Symbols: getFlowTypeOfReference, narrowTypeByTypeof, isTypeRelatedTo, getContextualType.
    Why and when: Core reading. One 50 000-line file holds Lesson 6.6's control-flow narrowing (getFlowTypeOfReference walks flow nodes backwards; narrowTypeByTypeof is the typeof guard of Algorithm 6.6.3), Lesson 6.5's structural assignability and Lesson 6.4's contextual typing. Search for the symbols; do not read linearly.
    Cited in: 02-classifying-type-systems, 04-bidirectional-typing, 05-subtyping, 06-flow-sensitive-typing, 07-gradual-typing

Official documentation and specifications

  • [C11] ISO/IEC 9899:201x (C11) committee draft N1570: §6.3 Conversions. link
    Why and when: §6.3.1.1 (integer promotions), §6.3.1.3 (signed and unsigned integers) and §6.3.1.8 (usual arithmetic conversions): the rules Algorithm 6.3.6 transcribes. Read with Lesson 6.3 §2.
    Cited in: 03-syntax-directed-checking

  • [CPP-Over] Working Draft, Programming Languages — C++: [over.match] (overload resolution) and [over.ics.rank]. link
    Why and when: The normative ranking of implicit conversion sequences (exact match, promotion, conversion; user-defined; ellipsis) and the "better viable function" relation. Read [over.ics.rank] with Lesson 6.3 §2.
    Cited in: 03-syntax-directed-checking

  • [JLS21-10] The Java Language Specification, Java SE 21: §10.5, Array Store Exception. link
    Why and when: The run-time check that makes covariant arrays safe (Lesson 6.2's box): Java's type system is sound only because this store check exists. Read with Lesson 6.2 §4.
    Cited in: 02-classifying-type-systems

  • [JLS21-5] The Java Language Specification, Java SE 21: Chapter 5, Conversions and Contexts. link
    Why and when: Java's conversions listed by context (assignment, invocation, casting, numeric promotion): a specification in which each checking position of Lesson 6.4 names the conversions it allows. Read §5.1.2 (widening primitive) and §5.6 (numeric contexts) with Lesson 6.3.
    Cited in: 03-syntax-directed-checking, 04-bidirectional-typing

  • [KOTLIN-Casts] Kotlin documentation: Type checks and casts (smart casts). link
    Why and when: The conditions under which Kotlin smart-casts a variable after an is check (the variable must be stable: a val, or a local var not captured by a lambda that modifies it). Read with Lesson 6.6 §6; not runnable in this course's container.
    Cited in: 06-flow-sensitive-typing

  • [KOTLIN-Generics] Kotlin documentation: Generics (declaration-site variance, type projections). link
    Why and when: Kotlin's out/in declaration-site variance and its use-site "type projections", with the rule that an out parameter may appear only in out-positions. Read with Lesson 6.5's variance section and compare with Java's wildcards in the javac box.
    Cited in: 05-subtyping

  • [POLONIUS] The Polonius book (rules/loans.md, rules/relations.md). link
    Why and when: The borrow check restated in Datalog over origins and loans; the naive rules R1–R8 are quoted in Lesson 6.8 §6. Read rules/loans.md after Algorithm 6.8.8 and compare "origins contain loans" with NLL's "regions contain points".
    Cited in: 08-places-and-references

  • [RFC2094] Rust RFC 2094: Non-lexical lifetimes. link
    Why and when: Core reading. Lifetimes as sets of CFG points computed by liveness and outlives constraints (a fixed point), then loans in scope as forward dataflow: Lesson 6.8's Algorithm 6.8.8. Read "Problem case #1–#4" first, then "Layer 1" and "Layer 5".
    Cited in: overview, 08-places-and-references

  • [RUSTC-DevGuide-Typeck] rustc dev guide: Type checking (hir-typeck) and MIR borrow check. link
    Why and when: How rustc's checker is organized (expectations, coercions, inference variables resolved at the end of each body) and, in the "MIR borrow check" chapter, how NLL runs on MIR. Read after Lessons 6.4 and 6.8.
    Cited in: 08-places-and-references

  • [SE0176] Swift Evolution SE-0176: Enforce Exclusive Access to Memory. link
    Why and when: The Law of Exclusivity (no overlapping accesses unless both are reads), enforced statically for locals and inout arguments and dynamically for class properties, globals and escaping captures. Read "Proposed solution" with Lesson 6.8's exclusivity section; it is the model for Pebble's rule E0414.
    Cited in: 08-places-and-references

  • [TR-Guide] The Typed Racket Guide: Occurrence Typing. link
    Why and when: Occurrence typing as programmers meet it: predicates such as number? refine the type of a variable in the branches of an if. Read with Lesson 6.6 §2 before [THF08].
    Cited in: 06-flow-sensitive-typing

  • [TS-Compat] TypeScript Handbook: Type Compatibility (A Note on Soundness). TypeScript 5.9. link
    Why and when: TypeScript's own list of places where the type system is intentionally unsound (method parameter bivariance, array covariance, optional parameters). Read with Lesson 6.2 §4.
    Cited in: 02-classifying-type-systems

  • [TS-Narrowing] TypeScript Handbook: Narrowing. TypeScript 5.9. link
    Why and when: Every narrowing form TypeScript supports (typeof, truthiness, equality, in, instanceof, assignments, discriminated unions, never), with the control-flow analysis explained informally. Read alongside Lesson 6.6 §7; the drill narrowing covers the typeof/equality/assignment subset.
    Cited in: 06-flow-sensitive-typing