Tellofou [CC BY-SA (https://creativecommons.org/licenses/by-sa/4.0)]
Timetable
Material
The literature depends on the particular subject of the seminar report. The following books are worth considering:
– "Lambda-Calculus and Combinators" by J. Roger Hindley and Jonathan P. Seldin
– "The Lambda Calculus, It's Syntax and Semantics" by Henk P. Barendregt
– "Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics"
– "Structural Proof Theory" by Sara Negri and Jan von Plato
– "Type-Theoretical Grammar" by Aarne Ranta
– "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt and Herman Geuvers. Available as an e-book (PDF chapters) from university's network:
https://helka.finna.fi/Record/helka.3247530
– "Type Theory and Functional Programming" by Simon Thompson, Addison-Wesley, 1991. Available online at:
https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf
– "Programming Language Foundations in Agda" by Philip Wadler, Wen Kokke, and Jeremy Siek. Freely available at:
https://plfa.github.io/
– "Types and Programming Languages" by Benjamin C. Pierce
– "Software Foundations vol. 2: Programming Language Foundations" by Benjamin C. Pierce et al. Freely available at:
https://softwarefoundations.cis.upenn.edu/plf-current/index.html
– "Homotopy Type Theory: Univalent Foundations of Mathematics". Freely available at:
https://homotopytypetheory.org/book/
The list above is very non-exhaustive. Students may have to search for relevant literature independently.
Conduct of the course
The outline of this seminar is based on the format of the CSM12116 Seminar on Model Checking (https://courses.helsinki.fi/en/csm12116/129911924).
In this seminar, the student needs to:
– Write a scientific style report with appropriate references and citations (cf. bachelor's thesis)
– Present the report to other students
– Write peer reviews on other students' reports and presentations
Most of the work in this seminar will be individual study. The first two meetings will include introductory lectures into Pure Untyped Lambda-Calculus and Type Theory. The final meetings will be presentations and discussion.
During the first meeting, we need to also decide some practicalities. We'd like to decide on the first meeting whether we want to have poster session(s) or oral presentations, and if the seminar should be extended to the intensive period in May. Programming projects are another option for interested students.
The course has an official Telegram group. See https://t.me/mltt2020
Description
No particular prerequisites are strictly necessary, though the topic requires mathematical maturity. Understanding of the following topics are strongly recommended:
- Introduction to Lambda Calculus from spring 2018. The intro lecture will revisit the topics of this course.
- Natural numbers and recursion
- Functional programming (not necessary if the student chooses a theoretical topic in pure type systems)
- First-order logic (e.g. Johdatus logiikkaan and/or Mathematical Logic), particularly natural deduction
Depending on the subject chosen for the seminar report, the following areas can be important:
- Category theory or abstract algebra
- Imperative or object-oriented programming
- Theory of computation (e.g. Laskennan mallit or Computability theory), especially decidability
This seminar is meant to be rather interdisciplinary. It covers the basics of type theory, including but not limited to:
- Type systems of programming languages
- Type inference, e.g.
- Algorithm W
- Type systems as formal deduction machineries
- Pure type systems, e.g.
- Simply typed lambda calculus
- The Hindley-Milner type system
- System F
- Calculus of (Inductive) Constructions
- Martin-Löf type theory
- Linear/affine type systems
- The Curry-Howard correspondence, especially the connection between intuitionistic logics and lambda calculi
- Use of type theory in formal methods, e.g.
- Interctive theorem proving (LCF or PAT style)
- Liquid types
- Type theories in classical mathematics
- Russel's Ramified Theory of Types
- Many-sorted logicsr
- Homotopy Type Theory
- Linguistic and/or philosophical applications
The literature depends on the particular subject of the seminar report. The following books are worth considering:
- "Lambda-Calculus and Combinators" by J. Roger Hindley and Jonathan P. Seldin
- "The Lambda Calculus, It's Syntax and Semantics" by Henk P. Barendregt
- "Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics"
- "Structural Proof Theory" by Sara Negri and Jan von Plato
- "Type-Theoretical Grammar" by Aarne Ranta
- "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt and Herman Geuvers. Available as an e-book (PDF chapters) from university's network:
- "Programming Language Foundations in Agda" by Philip Wadler, Wen Kokke, and Jeremy Siek. Freely available at:
- "Types and Programming Languages" by Benjamin C. Pierce
- "Software Foundations vol. 2: Programming Language Foundations" by Benjamin C. Pierce et al. Freely available at:
- "Homotopy Type Theory: Univalent Foundations of Mathematics". Freely available at:
The list above is very non-exhaustive. Students may have to search for relevant literature independently.
The course consists of:
- An introductory lecture
- Written seminar report
- A poster session and/or oral presentation (to be decided together with the participants)
Students may alternatively choose to perform an empirical project. For instance, a student may implement algorithm W in their programming language of choice and give a demo presentation.