Institutionernas doktorandkurser

Startdatum och periodicitet för kurser kan variera. Se detaljer för respektive kurs för aktuell information. För anmälan, kontakta respektive kursansvarig.


Functional Programming Languages with Linear Types

  • Kurskod: FDAT045
  • ECTS-poäng: 7,5
  • Institution: DATA- OCH INFORMATIONSTEKNIK
  • Forskarskola: Data- och informationsteknik
  • Periodicitet: LP4
  • Undervisningsspråk: Kursen kommer att ges på engelska
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)
Litteratur
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.
Föreläsare
Jean-Philippe Bernardy
Mer information
Jean-Philippe Bernardy
e-mail: bernardy@chalmers.se
phone: +46 31 772 10 51

Publicerad: to 14 okt 2010. Ändrad: on 23 aug 2017