Enrol

Timetable

These eight sessions will be held for the presentations:

– 21 April, 10:15 – 12:00
– 23 April, 10:15 – 12:00
– 28 April, 10:15 – 12:00
– 30 April, 10:15 – 12:00
– 5 May, 10:15 – 12:00
– 7 May, 10:15 – 12:00
– 12 May, 10:15 – 12:00
– 14 May, 10:15 – 12:00

The participants should prepare a preview version of their report and send it by email by the Friday before their presentation, so that the opponent will have a chance to prepare for the presentation. The slides or other material can optionally be submitted as well. The deadline for peer reviews will be Friday 22 May 23:59 and the deadline for the final submission is Friday 29 May 23:59.

We will probably hold the presentations in Zoom, unless the university opens its campuses in April, which seems unlikely. The participants should check the file sent by email, which contains the topics of the presentations, and the names of the speakers, opponents, and reviewers. NB: Please ignore the timetable below this text.

DateTimeLocation
Thu 12.3.2020
10:15 - 12:00
Thu 19.3.2020
10:15 - 12:00
Thu 26.3.2020
10:15 - 12:00
Thu 2.4.2020
10:15 - 12:00
Thu 16.4.2020
10:15 - 12:00
Thu 23.4.2020
10:15 - 12:00
Thu 30.4.2020
10:15 - 12:00

Other teaching

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.