Lambda calculus and category theory

This page is about applications of category theory to the lambda calculus and programming language theory generally. There are many relations between type theory and category theory . The most fundamental is equivalence between simply typed lambda calculus (with product types) and cartesian closed categories .

Literature

General references

  • Lambek & Scott, 1986: Introduction to Higher Categorical Logic, Part I. Cartesian closed categories and lambda-calculus
    • Early monograph by pioneers of subject
  • Crole, 1993: Categories for Types
    • Textbook coverage of correspondence between type theory and category theory
    • Thorough treatment of types (including polymorphism and higher-order polymorphism) but not computation (recursion, traces)
  • Jacobs, 1999: Categorical Logic and Type Theory
    • Dense and encyclopedic but carefully written

Variable binding, as in lambda abstraction

  • Fiore, Plotkin, Turi, 1999: Abstract syntax and variable binding (doi)
    • Influential paper whose “fundamental idea is to turn contexts [of variables] into the index category of presheaves”
    • Connection to species and operads described in: Fiore, 2005, invited talk: Mathematical models of computational and combinatorial structures (doi)

Subtypes, closely related to subobjects in topos theory

See also nLab pages on coercion and intrinsic/extrinsic views .

  • Reynolds, 1980: Using category theory to design implicit conversions and generic operators (doi, pdf, TCS.SE )
    • Reynolds, 1991: The coherence of languages with intersection types (doi)
    • Reynolds, 2000: The meaning of types from intrinsic to extrinsic semantics (doi, report )
  • Hofmann & Pierce, 1996: Positive subtyping (doi)
    • Extends implicit conversion with overwriting, or put, operators
  • Mellies & Zeilberger, 2015: Functors are type refinement systems (doi, pdf)
    • Early preprint: Mellies & Zeilberger, 2013: Type refinement and monoidal closed bifibrations (arxiv)

Fixed points (recursion) via traced monoidal categories

  • Hasegawa, 1997: Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi (doi, pdf)
    • First establishes correspondence between traces on cartesian monoidal categories and parametrized fixed point operators
    • Hasegawa, 1997, PhD thesis: Models of Sharing Graphs: A Categorical Semantics of let and letrec (pdf)
    • Hasegawa, 2003: The uniformity principle on traced monoidal categories (doi, pdf)
    • Hasegawa, 2007: On traced monoidal closed categories (doi, pdf)
  • Katis, Sabadini, Walters, 1997: Bicategories of processes (doi)
    • Based on bicategories but makes connection to traced monoidal categories
    • See also Carboni & Walter’s bicategories of relations
  • Jeffrey, 1998: Premonoidal categories and a graphical view of programs (online )
    • Denotational semantics of lambda calculus variant: maps text syntax to categories of mixed data flow and control flow graphs
    • Schweimeier, 2001, PhD thesis: Categorical and graphical models of programming languages (pdf)
      • Thesis by former student of Jeffrey
      • Ch. 6 is exposition of Jeffrey’s paper, see esp. new examples in Sec 6.2
  • Selinger, 1999: Categorical structure of asynchrony (doi, pdf)
    • Good exposition of traced monoidal categories with many examples
  • Simpson & Plotkin, 2000: Complete axioms for categorical fixed-point operators (doi, pdf)
  • Benton & Hyland, 2003: Traced premonoidal categories (doi, pdf)
    • Extends Hasegawa’s correspondence to premonoidal categories
  • Hyland, 2008: Abstract and concrete models for recursion (pdf, slides)
    • The exposition is lacking, but the bibliography is helpful
    • Hyland & Power, 2000: Symmetric monoidal sketches (pdf)
    • Hyland & Power, 2004: Symmetric monoidal sketches and categories of wirings (ps )
  • Ponto & Shulman, 2014: Traces in symmetric monoidal categories (doi, arxiv)
    • Expository paper but focused on topology, not computation
    • Nice summary of connection between traces and fixed points (Sec 1)

Miscellaneous papers on category theory and computing, not necessarily related to the lambda calculus:

  • Goguen, 1975: Discrete-time machines in closed monoidal categories I (doi, pdf)
    • Title notwithstanding, this paper has no sequel
  • Pavlovic, 2013: Monoidal computer I: Basic computability by string diagrams (doi, arxiv)
  • Pavlovic, 2014: Monodial computer II: Normal complexity by string diagrams (arxiv)
  • Pavlovic & Yahia, 2017: Monoidal computer III: A coalgebraic view of computability and complexity (arxiv)
  • Pavlovic, 2022: Categorical computability in monoidal computer: Programs as diagrams (arxiv)