Lambda calculus, types and foundations of programming languages

The course is included in the degree programme Logic, Master's (120 credits) programme (H2LOG) and can also be given as a freestanding course.

For admission to the course successful completion of Logical theory (LOG111), or the equivalent, is

required.

English 6 or equivalent is also required.

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 (such as 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).

On successful completion of the course the student will be able to:

Knowledge and understanding

• demonstrate advanced knowledge and understanding of the theoretical foundations of functional programming languages

• apply a variety of tools and techniques for analysing key properties of functional programming languages, such as termination, confluence, computational strength.

Competence and skills

• formulate and present proofs of the most important results in the course as well as of lemmas that are used in the proofs,

• apply the theoretical results and methods of the course,

Judgement and approach

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

Teaching is given in the form of lectures and individual assignments.

Language of instruction: English

If a student who has been failed twice for the same examination element wishes to change examiner before the next examination session, such a request is to be granted unless there are specific reasons to the contrary (Chapter 6 Section 22 HF).

If a student has received a certificate of disability study support from the University of Gothenburg with a recommendation of adapted examination and/or adapted forms of assessment, an examiner may decide, if this is consistent with the course’s intended learning outcomes and provided that no unreasonable resources would be needed, to grant the student adapted examination and/or adapted forms of assessment.

If a course has been discontinued or undergone major changes, the student must be offered at least two examination sessions in addition to ordinary examination sessions. These sessions are to be spread over a period of at least one year but no more than two years after the course has been discontinued/changed. The same applies to placement and internship (VFU) except that this is restricted to only one further examination session.

If a student has been notified that they fulfil the requirements for being a student at Riksidrottsuniversitetet (RIU student), to combine elite sports activities with studies, the examiner is entitled to decide on adaptation of examinations if this is done in accordance with the Local rules regarding RIU students at the University of Gothenburg.

The grading scale comprises: Pass with Distinction (VG), Pass (G) and Fail (U). All parts in the

examination (written examination, oral presentation, and homework assignments) should be approved

by examiner to get a passing grade. To receive a Pass with distinction, it is furthermore required that

the written examination receives the assessment Pass with distinction.

The results of and possible changes to the course will be shared with students who participated in the evaluation and students who are starting the course.

The course requires access to a computer (or the equivalent) with Internet connection.