Monday, 21 June 2010

Reference request for type theory

The kind of type theory you're asking about, Russell's simple theory of types, is from about the early 1900's. Here's a reference:



  • Russell, Bertrand: Mathematical Logic as Based on the Theory of Types. Amer. J. Math. 30 (1908), no. 3, 222--262.

Recent work in type theory is somewhat different, continuing the tradition of Per Martin-Löf. In addition to his work (referenced by Andrej), I would also recommend the following book by Luo:



  • Luo, Zhaohui: Computation and reasoning. A type theory for computer science. International Series of Monographs on Computer Science, 11. The Clarendon Press, Oxford University Press, New York, 1994. xii+228 pp. ISBN: 0-19-853835-9.

For the relation between set theory, type theory, and category theory, you might want to have a look at this preprint by Steve Awodey.



There's also an n-lab page, and the type theory page at Stanford Encyclopedia of Philosophy has a reference section.

No comments:

Post a Comment