Course syllabus

Jump to today

Lambda calculus, types and foundations of programming languages

This course is part of the Master's Programme in Logic and available as a free standing course.

Course content

Lambda calculus is a model of computation that provides a mathematical foundation of functional programming languages. Its typed formulations have been used to investigate the computational content of logical and mathematical proofs, via the celebrated Curry-Howard correspondence paradigm.

The course covers central topics and results on the subject area. Specifically, the course content:

  • introduces the untyped lambda calculus and its basic properties
  • analyses various standard type systems (e.g., the simply typed lambda calculus, systems T, system F, and PCF).
  • provides key proof methods for establishing abstract properties of type systems, as well as extracting the computational content of mathematical theories (examples are realisability techniques and logical relations).

Teachers

The course will be taught by Gianluca Curzi. You can contact Gianluca by email, gianluca.curzi@gu.se

Examiner

The course examiner for this course is Graham E Leigh.

Registration

You will be able to register for the course one week before it starts. When you have registered for the course you will get access to more course information. You can find information regarding registration here.

Schedule

The course starts XX and meets each XX. Details about the schedule will be addressed at the first course meeting.

Below are links to the schedule in TimeEdit. There are two links - one which require login (your GU account) and one that does not. The link requiring login shows some additional information.

Schedule:  without login and with login.

The schedule is preliminary until two weeks before the course starts. Please also note that the schedule is a "living document" and could be subject to changes throughout the semester. Make a habit of checking it every once in a while!

Literature

  1. Main reference for the students (handbook): Lectures on the Curry-Howard Isomorphism, by Morten Heine Sørensen, Pawel Urzyczyn (2006).
  2. Reference on lambda calculus and simple types (handbook): Lambda-Calculus and Combinators - An Introduction, by J. Roger Hindley and Jonathan P. Seldin (2006).
  3. Reference on PCF and domains (handbook): Domains and Lambda-Calculi, by Di Roberto M. Amadio, Pierre-Louis Curien (1998).

Lecture plan

Lecture 1:

  • Untyped lambda calculus, part 1: lambda terms, beta reduction, extensionality, confluence (Chapter 1 of Reference 2)

Lecture 2: 

  • Untyped lambda calculus, part 2: expressivity and undecidability (Section 1.7 of Reference 1; for more details see also Chapter 4 and 5 of Reference 2)
  • Simply typed lambda calculus, part 1: Church vs Curry typing, normalisation, expressivity (Chapter 3 of Reference 1; for more details see also Chapter 10 and 12) 

Lecture 3:

  • Simply typed lambda calculus, part 2: normalisation for simply typed lambda calculus (Section 3.5 of Reference 1 + document "Normalisation" in Files)

Lecture 4:

  • Expressibility and decidability (Section 3.7 of Reference 1)
  • Curry-Howard isomorphisms: historical facts, applications and extensions (Sections 4.1-5 of Reference 1) 
  • System T, part 1: type system and historical remarks, normalisation (Sections 10.2-10.3 of Reference 1)

Lecture 5:

  • System T, part 2: first-order arithmetic, expressibility via realisability and applications (Sections 9.2, 9.4, 9.5, 10.4 of Reference 1)

Lecture 6:

  • System F, part 1: type system, historical remarks, recursion via polymorphism (Sections 3, 4.3 of document "System F" in Files) 

Lecture 7:

  • System F, part 2: normalisation via reducibility candidates (Sections 4.5-4.6 of document "System F" in Files) 

Lecture 8:

  • PCF and its denotational semantics, part 1: type system, operational semantics, omega-cpos and continuity (Chapter 2, and Sections 3.1-3.2 of document "PCF" in Files) 

 Lecture 9: 

  • PCF and its denotational semantics, part 2: the Scott model of PCF, soundness and computational adequacy (Sections 3.3-3.4, and Chapters 4 and 5 of document "PCF" in Files)

Examination

There will be one sit down written examination. This is an individual closed book exam and you are not allowed to bring any text, book, computer or other device to the exam. Please read the general information about exams.

The hand-in problems and assignments are not obligatory to pass the course, but we strongly recommend students to take the opportunity to get feedback on their solutions.

Learning outcomes

On successful completion of the course LOG330 Specialization in Logic 4 the student will be able to:

Knowledge and understanding

  • demonstrate in-depth knowledge and understanding within some of the subareas or applications of logic,
  • relate the newly acquired specialist knowledge with the fundamental areas of logic,

Competence and skills

  • formulate and present proofs of the most important results in the course as well as of lemmas that are used in proofs (upon theoretical specialisation),
  • apply logical results and methods outside pure research (upon specialisation in an applied field),

Judgement and approach

  • critically discuss, analyse and evaluate results in the course as well as their applications,

demonstrate the ability to work over disciplinary borders.

See the course syllabus for more information.

Course evaluation

Students who are currently taking the course or have completed it will be given the opportunity to express their views and share their experiences in an anonymous course evaluation. A compilation of the course evaluation and the course coordinator’s reflections on it will be made available to the students within reasonable time after the end of the course. The next time the course is taught the compilation and any measures based on it will be presented to the students.

Special pedagogical support

If you have a disability and are in need of special pedagogical support please see the information available at the student portal. 

Contact information

  • Course coordinator Ivan Di Liberti,  ivan.di.liberti@gu.se answers questions about the course content, literature and schedule.
  • Education administrator Sandra Schriefer, sandra.schriefer@gu.se  answers questions about registration, study interruptions, study breaks, certificates, etc. 
  • Program Coordinator Ivan Di Liberti,  ivan.di.liberti@gu.se is responsible for programme issues and study guidance for students of the programme.
  • Education Coordinator Andreas Ott, andreas.ott@gu.se 

Plagiarism and academic integrity

Please take the time to go through the module Academic Integrity 1 to make sure that you understand what plagiarism is, why one should not plagiarise, and what happens if one does plagiarise.

Student information

Learn Canvas

Checklist for new students

Student Portal

Welcome to the department of Philosophy, Linguistics and Theory of Science

Study Environment and Rules

Plagiarism and academic integrity 

Course summary:

Course Summary
Date Details Due