Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

External References

Books

  • Pierce, B. C. (2002). Types and programming languages. MIT press.
  • Pierce, B. C. (Ed.). (2024). Advanced topics in types and programming languages. MIT press.
  • Harper, R. (2016). Practical foundations for programming languages. Cambridge University Press.
  • Jones, R., Hosking, A., & Moss, E. (2023). The garbage collection handbook: the art of automatic memory management. Chapman and Hall/CRC.

Algorithm W

  • Robin Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, 1978.
  • François Pottier and Didier Rémy. The Essence of ML Type Inference. In Advanced Topics in Types and Programming Languages, MIT Press, 2005.

System F and System Fω

  • Mark P. Jones. Typing Haskell in Haskell. Haskell Workshop, 1999.
  • Müller, M. (1998, August). Notes on HM (X).
  • Odersky, M., Sulzmann, M., & Wehr, M. (1999). Type inference with constrained types. Theory and practice of object systems, 5(1), 35-55.
  • Faxén, K. F. (2002). A static semantics for Haskell. Journal of functional programming, 12(4-5), 295-357.
  • Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference. ICFP 2019.
  • Jana Dunfield and Neelakantan R. Krishnaswami. Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism. ICFP 2013.
  • Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference. ECOOP 2022.
  • Roger Bosman, Georgios Karachalias, Tom Schrijvers. No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. ITP 2023.

Dependent Types

  • Chris Bailey. Type Checking in Lean 4. https://ammkrn.github.io/type_checking_in_lean4/
  • Xu Xue and Bruno C. d. S. Oliveira. Contextual Typing. ICFP 2024.

Row Polymorphism

  • Didier Rémy. Type Inference for Records in a Natural Extension of ML. In Theoretical Aspects of Object-Oriented Programming, MIT Press, 1994.
  • Daan Leijen. Extensible Records with Scoped Labels. Trends in Functional Programming, 2005.

Algebraic Effects and Handlers

  • Gordon Plotkin and John Power. Algebraic Operations and Generic Effects. Applied Categorical Structures, 2003.
  • Gordon Plotkin and Matija Pretnar. Handlers of Algebraic Effects. ESOP 2009.
  • Matija Pretnar. An Introduction to Algebraic Effects and Handlers. ENTCS, 2015.

Call-by-Push-Value

  • Paul Blain Levy. Call-by-Push-Value: A Subsuming Paradigm. TLCA 1999.
  • Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis. Springer, 2003.

Pattern Matching

  • Luc Maranget. Warnings for Pattern Matching. Journal of Functional Programming, 17(3), 387-421, 2007.
  • Luc Maranget. Compiling Pattern Matching to Good Decision Trees. ML Workshop, 2008.

Refinement Types

  • Tim Freeman and Frank Pfenning. Refinement Types for ML. PLDI 1991.
  • Patrick M. Rondon, Ming Kawaguchi, and Ranjit Jhala. Liquid Types. PLDI 2008.
  • Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton Jones. Refinement Types for Haskell. ICFP 2014.