nLab Andrew Pitts

Andrew Mawdesley Pitts is a professor of theoretical computer science at Cambridge. His thesis was on the theory of triposes; he studies semantic of programming languages, type theory, symbolic computation etc.

• webpage

Selected writings

• Nontrivial power types can’t be subtypes of polymorphic types, ps.gz

• The theory of triposes, 1981, thesis, pdf

• Tripos theory in retrospect, pdf

On Gabriel-Ulmer duality:

• Michael Makkai, Andrew Pitts, Some results on locally finitely presentable categories, Trans. Amer. Math. Soc. 299 (1987) 473-496 [doi:10.2307/2000508, pdf, MR88a:03162]

On categorical semantics and the categorical model of dependent types:

• Andrew M. Pitts, Categorical logic, in Handbook of Logic in Computer Science 5 Oxford Univ. Press (2000) 39-128 [doi:10.1093/oso/9780198537816.003.0002, pdf, MR1859470]

On denotational semantics and domain theory:

• Andrew M. Pitts, Lecture Notes on Denotational Semantics (2012) [pdf, pdf]

On quotient types, inductive types and inductive-inductive types:

• Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp, Quotients, inductive types, and quotient inductive types, Logical Methods in Computer Science 18 2 (2022) lmcs:7076 [arXiv:2101.02994, doi:10.46298/lmcs-18(2:15)2022]

category: people