Tüübiteooria / Type Theory

Üldinfo / General information

Aine kood: MTAT.05.105
Lektorid:
- Varmo Vene
- James Chapman
Ainepunkte: 6 EAP
Loengute toimumise aeg/koht:

Esmaspäev, kell 12.15 - 14.00, L405
Teisipäev, kell 14.15 - 16.00, L403 [March 16]
Teisipäev, kell 16.15 - 18.00, L612 [Feb.16, March 16, April 6, April 20]
Kolmapäev, kell 12.15 - 14.00, L612 [Feb.17, March 17, April 7, April 21]
Neljapäev, kell 10.15 - 12.00, L111 [Feb.11, Feb.18, Feb.25]
Neljapäev, kell 10.15 - 12.00, L403 [since Match 11]

Kirjandus:
- 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.
Eksam:
- 27.05, kell 10.15 - 14.00, L330
- 03.06, kell 10.15 - 14.00, L330

Lecture slides

08. 02 - [VV] Introduction, untyped λ-calculus (lecVV1.pdf).
11. 02 - [VV] Simply-typed λ-calculus (lecVV2.pdf).
15. 02 - [JC] Introduction to dependently typed programming (lecJC1.pdf).
16. 02 - [JC] Agda syntax and basic definitions (lecJC2.pdf, Live.agda).
17. 02 - [JC] Lab session.
18. 02 - [JC] Lab session.
22. 02 - [VV] Simply-typed λ-calculus (cont.).
25. 02 - [VV] Propositional logic (lecVV3.pdf).
08. 03 - [VV] Curry-Howard correspondence, 1st- and 2nd-order predicate logic.
11. 03 - [VV] Second-order λ-calculus (lecVV4.pdf).
15. 03 - [JC] Intuitionistic propositional logic (lecJC3.pdf, Live2.agda).
16. 03 - [JC] Intuitionistic predicate logic (NatFeedback.agda).
16. 03 - [JC] Lab session.
17. 03 - [JC] Lab session.
22. 03 - [VV] Second-order λ-calculus (cont.).
25. 03 - [VV] Type inference; Hindley-Milner type system (lecVV5.pdf).
29. 03 - [VV] The λ-cube; pure type systems (lecVV6.pdf).
01. 04 - [VV] The λ-cube; pure type systems (cont.).
05. 04 - [JC] Evaluating simple languages (Exp1.agda, Exp2.agda, Exp3.agda, Exp4.agda, Exp5.agda, Exp6.agda).
06. 04 - [JC] Evaluating simple languages continued, renaming and substitution (Exp6a.agda, Exp6b.agda).
07. 04 - [JC] Lab session.
08. 04 - [JC] Lab session.
12. 04 - [VV] The λ-cube; pure type systems (cont.).
19. 04 - [JC] Renaming and substitution for λ-calculus (ExpRenSub.agda, LamRenSub.agda).
20. 04 - [JC] Evaluating and type checking λ-calculus (WellTypedComb.agda, WellTypedLam.agda, WellTypedLam2.agda).
21. 04 - [JC] Evaluating and type checking λ-calculus (cont.).
22. 04 - [JC] Lab session.
26. 04 - [VV] Subtyping (lecVV7.pdf).
29. 04 - [VV] Subtyping (cont.).
06. 05 - [VV] Subtyping (cont.).
10. 05 - [JC] Lab session.

Assignments

BoolQuestions.agda (deadline March 8).
NatQuestions.agda (deadline March 8).
LogicQuestions.agda (deadline April 1).
FinQuestions.agda (deadline April 1).
CombQuestions.agda (deadline April 18).
TTexercises.pdf, TTexercises.tex, (deadline May 6).
TCQuestions.agda (deadline May 16).

Useful links

Varmo Vene