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)
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 )
- 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)
- 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)