lunduniversity.lu.se

Computer Science

Faculty of Engineering, LTH

Denna sida på svenska This page in English

Type Systems

News

  • May 29: Added slides for the recursive types and featherweight java seminars
  • May 14: Added exercises from the seminar on subtyping
  • April 26:: The slides and exercise for yesterdays seminar have been added to the schedule. NB! We have no exercises planned for May. If you have questions post them on the mail list or request an exercise session and we can schedule one.
  • April 18: Please fill in the doodle for when to have the exercise in week 17 here (unfortunately, Friday 15-17 collides with the Scala course in week 17). From now on we will try to have one joint exercises session for programming exercises and exercises from the previous seminar. Also, the schedule has been updated with todays slides and exercises.
  • April 16: Next programming exercise is on Friday (20/4) 15-17 in Glasburen.
  • March 29: The weekly seminar time has been changes to 15:00-16:30 (NB! Prick prick). Also, please select possible slots for the next programming exercise here.
  • March 14: The weekly seminar time has been changed to 14:30-16:30 and a weekly exercise session starting at 13:15 before the seminar has been added. Also, the next programming session has been booked for Tue March 20 15:15-17:00 (see schedule).
  • Feb 29: Todays exercises and dates for first programming session and an extra exercise session have been added to the schedule.
  • Feb 22: Please fill in this Doodle to indicate which slots that would suit you best for the first programming session. Also, todays selection of exercises and dates have been added to the schedule.
  • Feb 14: New start time for the first seminar: Feb 22 15:15-17:00 in Glasburen.
  • Feb 11: There is now a mail list for the course called [course-type-systems]. You can administrate your membership of the list, and view the archive, here.
  • Feb 11: The LAMP links broke due to a reorganization of their web server. The links should work again now, but if this happens again you can find the content of the LAMP pages here.

Description

"The study of type systems -- and of programming languages from a type theoretic perspective -- has become an energetic field with major applications in software engineering, language design, high-performance compiler implementation, and security..." (Types and Programming Languages, Pierce).

In this seminar course, participants will lean about type systems and their properties. The content of the course is heavily influenced by the Software foundations course given at EPFL by Martin Odersky, and the content of the Types and Programming Languages book by Benjamin Pierce.

When

Spring 2012, Starting on February 22nd (see the schedule below for details). To sign up for the course email one of the course organizers.

Credits, Workload and Form

The course includes eleven theoretical seminars lead by participants. Each participant expecting credits is expected to lead at least one of these seminars together with another participant. Each seminar is connected to one or two chapters in the course book and course slides. Participants organizing seminars are expected to select exercises from relevant parts of the course book for the remaining participants to solve for the upcoming seminar.

In addition to the seminars and the pen and paper exercises, the course also includes seven programming sessions. The exercises in these sessions will be done in the Scala language. There will be at least an initial joint programming session for the first of these exercises. This session will focus on Scala and on getting started with the library used for the remaining exercises.

Assuming that there is one programming session for each programming exercise, there will be 19 scheduled seminars/sessions á 2 h. The number of exercises will be settled as the course moves along, but it should be assumed that both the theoretical and the programming exercises will require significant work by participants. Additionally, participants should prepare at least one seminar. The course has for this reason been approximated to 7.5hp.

Participants following the course without getting credits are not expected to lead seminars, but are welcome to do so if they like.

Course Organizers

Jörn Janneck (AT cs.lth.se), Emma Söderberg (AT cs.lth.se)

Course Material

  • Book:Types and Programming Languages (TAPL) Benjamin C. Pierce. You can find more info here.
  • Slides: We use the slides of the Software Foundations (SF) course at EPFL which you can find here.
  • Programming exercises: We use the programming exercises from the Software Foundations course at EPFL which you can find here.

Prerequisites

The focus of this course is type systems and for this reason we have made some of the material of TAPL and SF into prerequisites. Participants should be familiar with the content of Chapter 2,3 and 5 in TAPL, and the SF slides for week 1-4 (these more or less follow TAPL). Also, it may help to look at a Scala tutorial before the course starts to get some basic knowledge of Scala for the programming exercises. You can find more information about Scala here.

Schedule

Missing dates will be discussed at the first seminar.

Seminars
  • Date: Wed Feb 22 15:15-17:00 (Glasburen)
    S1: Introduction and walk-through of prerequisites (Ch 2,3,5 + W 1-4)
    Seminar leaders: Jörn Janneck, Emma Söderberg
    Type Systems 00 - Administrivia
    Type Systems 01 - Preliminaries
    Type Systems 02 - Basic Concepts
    Exercises: 3.2.5 (p27), 3.3.4 (p31)
  • Date: Wed Feb 29 15:15-17:00 (Glasburen)
    S2: Introduction and walk-through of prerequisites (Ch 2,3,5 + W 1-4)
    Seminar leaders: Emma Söderberg, Jörn Janneck
    The remainder of the previous seminar (S1), starting from operational semantics.
    Type Systems 02b - Derivation
    Exercises: 3.5.5 (p38), 3.5.13 (p40), 3.5.16 (p42), 5.3.6 (p72)
  • Date: Wed Mar 7 15:15-17:00 (Glasburen)
    S3: Types and Simply-typed Lambda Calculus (STLC) (Ch 8,9 (Not: 9.3-..)+ W 5)
    Seminar leaders: Usman Mazhar Mirza
    Type Systems 03 - Types
    Exercises: 8.2.3 (p94), 8.3.6 (p98), 8.3.7 (p98), 9.2.2 (p103), 9.2.3 (p103)
  • Date: Wed Mar 14 15:15-17:00 (Glasburen)
    S4: Properties of Type Systems (Ch 9.3 + W 6,7 (Not slides on: equivalence, STLC extensions))
    Seminar leaders: Gustav Cerdersjö, Niklas Fors
    Type Systems 04 - Properties
    Exercises: 9.3.2 (p104), 9.3.9 (p107)
  • Date: Wed Mar 21 14:30-16:30 (Glasburen)
    S5: STLC extensions (Ch 11 + W 7,8 (Not slides on: equivalence))
    Seminar leaders: Gustav Cerdersjö, Niklas Fors
    Type Systems 05 - STLC Extensions
    Exercises: 11.5.2 (p125), 11.9.1 (p134)
  • Date: Wed Mar 28 14:30-16:30 (Glasburen)
    S6: Recursion, References and Stores (Ch 11,13 + W 8)
    Seminar leaders: Mehmet Ali Arslan
    Type Systems 06 - Stores
    Exercises: 11.11.1 (p144), 13.4.1 (p164), 13.5.2 (p167))
  • Date: Wed April 18 15:00-16:30 (Glasburen)
    S7: Type reconstruction (Ch 22 + W 9)
    Type Systems 07 - Type Reconstruction
    Exercise: Read through the proofs for 22.3.5, 22.3.7, and 22.4.5
    Seminar leader: Jörn Janneck
  • Date: Wed April 25 15:00-16:30 (Glasburen)
    S8: Parameterized Polymorphism (Ch 23 + W 9)
    Type Systems 08 - Polymorphism
    Exercises: The proofs for theorems 23.5.1 and 23.5.2
    Seminar leader: Dzmitry Sledneu
  • Date: Wed May 2 15:00-16:30 (Glasburen)
    S9: Subtyping (Ch 15,16 + W 11)
    See slides from the EPFL course on subtyping
    Seminar leader: Hans Gylling
    Read through the proofs for lemmas and theorems 15.3.3, 15.3.4, 15.3.5, and 15.3.7. Do exercises 15.5.2, 15.5.3, 16.1.2, and 16.2.5.
  • Date: Wed May 9 15:00-16:30 (Glasburen)
    S10: Objects (Ch 18 + W 12)
    See slides from the EPFL course on objects
    Seminar leaders: Emma Söderberg, Jörn Janneck
    No exercises this week
  • Date: Wed May 16 15:00-16:30 (Glasburen)
    S11: Recursive Types (Ch 20 (+ Ch 21))
    Type Systems 11 - Recursive Types
    Seminar leader: Linus Åkesson
  • Date: Wed May 23 15:00-16:30 (Glasburen)
    S12: Featherweight Java (Ch 19 + W 13), Paper
    Type Systems 12 - Featherweight Java
    Seminar leader: Amr Ergawy
  • Date: Wed May 30 15:00-16:30 (Glasburen)
    S13: Featherweight Scala (W 14)
    Seminar leaders: Flavius Gruian
Exercise Sessions

No exercises are planned for May. In case you would like to have one, send an email to the mail list and we can schedule one.

  • Date: Wed Mar 7 13:15-15:00 (Glasburen)
    We focus on the exercises from S1 and S2.
  • Date: Wed Mar 14 13:15-15:00 (Glasburen)
    We focus on the exercises from S3.
  • Date: Wed Mar 21 13:15-14:30 (Glasburen)
    We focus on the exercises from S4.
  • Date: Wed Mar 28 13:15-14:30 (Glasburen)
    We focus on the exercises from S5.
  • Date: Wed April 18 13:15-15:00 (Glasburen)
    We focus on the exercises from S6.
  • Date: Wed April 25 13:15-15:00 (Glasburen)
    We focus on the exercises from S7.
Programming Sessions

No exercises are planned for May. In case you would like to have one, send an email to the mail list and we can schedule one.