Some resources for the Types course, MT4592/MT5592

in http://www.cs.man.ac.uk/~petera/Types_course/types_resources.html

Books etc

• Barendregt, H.
  • The Lambda Calculus. Its Syntax and Semantics, North Holland, 2nd edition (1984)
  • Lambda calculi with Types. In Handbook of Logic in Computer Science, Vol 2, OUP, (1992), pp 117-309.
  • Introduction to Generalized Type Systems, Journal of Functional Programming, 1 (1991), pp 125-154.
• Beeson,M.J.
  • Foundations of Constructive Mathematics, Springer (1985)
• Bishop, E.
  • Foundations of Constructive Analysis, McGraw-Hill (1967)
• Bishop, E. and Bridges, D.
  • Constructive Analysis, Springer (1985)
• Curry, H.B.
  • Foundations of mathematical Logic, McGraw-Hill (1963)
• Curry, H.B. and Feys, R.
  • Combinatory Logic, Vol 1, North Holland, 2nd edition (1968)
• Girard, J-Y., Lafont, Y. and Taylor, P.
  • Proofs and Types, CUP (1996)
• Hindley, J.R.
  • Basic Simple Type Theory, CUP (1997)
• Hindley, J.R. and Seldin, J.P.
  • Introduction to Combinators and Lambda Calculus, LMS student texts 1, CUP (1986)
• Krivine
  • Lambda Calculus, Types and Models (1993)
• Luo, Z.
  • Computation and Reasoning: A Type Theory for Computer Science, OUP (1994)
• Martin-Lof, P.
  • Intuitionistic Type Theory, Bibliopolis (1984)
• Mitchell, J.C.
  • Foundations for Programming Languages, MIT Press (1996)
• Pierce, B.C.
  • Types and programming Languages, MIT Press (2002)
• Prawitz, D.
  • Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell (1965)
• Simmons, H.
  • Derivation and Computation, CUP (2000)
• Sorensen, M. H. B. and Urzyczyn, P.
  • Lectures on the Curry-Howard Isomorphism
• Nordstrom, B., Petersson, K. and Smith, J.,
  • Programming in Martin-Lof's Type Theory. An Introduction, OUP (1990)
• Stenlund, S.
  • Combinators, Lambda Terms and Proof Theory, Reidel (1972)
• Thompson, S.
  • Type Theory and Functional Programming, Addison Wesley (1991)
• Troelstra, A.S. and Schwichtenberg, H.
  • Basic Proof Theory, CUP (1996)
• Troelstra, A.S. and van Dalen, D.
  • Constructivism in Mathematics (2 volumes), North Holland (1988)
• Turner, R.
  • Constructive Foundations for Functional Languages, McGraw-Hill, (1991)

Online Resources

• Lecture notes - by Ralph Loader (39 pages)
  
• The impact of the lambda calculus in logic and computer science - by Henk Barendregt
• Foundations of Functional Programming Lecture Notes, by Larry Paulson (54 pages)
• Lambda Calculi with Types, by Henk Barendregt, Handbook of Logic in Computer Science, Volume II (193 pages)
• Proof Assistants using Dependent Type Systems , by Henk Barendregt and Herman Geuvers, Handbook of Automated Reasoning, edited by Alan Robinson and Andrei Voronkov, 2001, (89 pages)
• Lecture notes, by Luke Ong (89 pages)
• Lectures on the Curry-Howard Isomorphism by Morten Heine B. Sorensen (University of Copenhagen), Pawel Urzyczyn (University of Warsaw) (275 pages)
• Type Systems, By Luca Cardelli (42 pages)
  An introductory overview
• Lecture Notes by H. Schwichtenberg
• Introduction to the Literature on Semantics, by Gary T. Leavens