Departments' graduate courses

Course start and periodicity may vary. Please see details for each course for up-to-date information. The courses are managed and administered by the respective departments. For more information about the courses, how to sign up, and other practical issues, please contact the examiner or course contact to be found in the course information.


Functional Programming Languages with Linear Types

  • Course code: FDAT045
  • Course higher education credits: 7.5
  • Department: COMPUTER SCIENCE AND ENGINEERING
  • Graduate school: Computer Science and Engineering
  • Course is normally given: LP4
  • Language: The course will be given in English
TOPIC
Girard proposed Linear Logic (LL) as a constructive treatment of classical logic.

Under the Curry-Howard lens, LL can be seen as
a resource-aware (RAW) type-system for functional programs (FP);
a type-system for concurrent programs
The goal of the course is to gain familiarity with LL, and experiment with it, or variants of it, as a RAWFP language.

ORGANIZATION:
The course will be organized as a tutorial on programming language research. The course will start with one (or more if needed) seminar on the computational interpretation of intuitionistic linear logic; based on Abramsky (93) and Wadler (12). After the introductory lecture(s) the students are expected to identify their interests in the field, and set their goals for the course accordingly.

Then, during weekly seminars students will present the status of their progress as well as pending problems, and receive feedback from the group. Group work and collaboration between groups is encouraged.

A typical project will consist of:
Given the student's topic of interest, do a literature search, identify the most relevant paper, read it and digest it (40h)
Implement a prototype of a feature/compilation phase/...(95h)
Present their findings in a seminar (20h)
Variants on this scheme can be accepted as a project, if motivated. For example a theoretically-inclined student might skip the implementation but read two papers, present them at separate seminars and synthesize them in a report.

More information
To get 7.5 credits, you are expected to: Attend the seminars (15h)
Identify a suitable project (read material, discuss with the group, etc. as needed) (15h)
Complete the project of their choice (155h).
Prepare to present their intermediate findings/blocking issues at bi-weekly seminars/meetings (15h)
Literature
Linear Logic, Girard (87)
Linear Logic Primer, DiCosmo http://www.dicosmo.org/CourseNotes/LinLog/CorsoPisa.pdf Has a good section on why to study LL
Computational Interpretations of Linear Logic, Abramsky (93)
Propositions as Sessions, Wadler (12)
A Type System for Bounded Space and Functional In-Place Update, Hoffmann (00)
Function Interface Models for Hardware Compilation. Ghica.
Uses ideas from LL to compile higher-order functional programs to hardware.
Lecturers
Jean-Philippe Bernardy
More information
Jean-Philippe Bernardy
e-mail: bernardy@chalmers.se
phone: +46 31 772 10 51

Page manager Published: Tue 22 Aug 2017.