Institute of Computer Science
  1. Courses
  2. 2019/20 fall
  3. Type Theory (MTAT.05.105)
ET
Log in

Type Theory 2019/20 fall

  • Home Page
  • Lectures
  • Exercises

General information

  • Course: Type Theory, MTAT.05.105 (6ECTS)
  • Lecturers: Varmo Vene, Kalmer Apinis

Lectures:

  • Wednesday, 10.15-12.00, Liivi 2-612
  • Friday, 16.15-18.00, Liivi 2-612

Exam:

  • Format: Home exam (24h to submit written part + 10min oral explanations)
  • Date&Time:
    • 17.12.2019 (14.00 - 16.00)
    • 22.01.2020 (14.00 - 16.00)
  • Mostly theory exercises, very few coq exercises.
  • Requirements for attending the exam: complete >85% of homework exercises (theory+coq).

Recources/Literature:

  • S. Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991.
  • B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
  • B. C. Pierce. Advanced Topics in Types and Programming Languages. MIT Press, 2004.
  • M. H. Sorensen, P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. DIKU Rapport 98/14, 1998.
  • H. Barendregt. Lambda calculi with types. In: Handbook of Logic in Computer Science. Oxford University Press, 1992.
  • B. C. Pierce et al, Software Foundation Vol. 1: Logical Foundation (slides)
  • B. C. Pierce et al, Software Foundation Vol. 2: Programming Language Foundation (slides)

Links

  • Type Theory Course 2011
  • Institute of Computer Science
  • Faculty of Science and Technology
  • University of Tartu
In case of technical problems or questions write to:

Contact the course organizers with the organizational and course content questions.
The proprietary copyrights of educational materials belong to the University of Tartu. The use of educational materials is permitted for the purposes and under the conditions provided for in the copyright law for the free use of a work. When using educational materials, the user is obligated to give credit to the author of the educational materials.
The use of educational materials for other purposes is allowed only with the prior written consent of the University of Tartu.
Terms of use for the Courses environment