Kaisa_2012_3_photo by Veikko Somerpuro

Enrol
10.2.2020 at 09:00 - 30.4.2020 at 23:59

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.