ASLL-09

From PLSwiki

Jump to: navigation, search

Contents

1 Advanced Seminar in Linear Logic, Spring 2009
2 Practical and administrative matters
3 Topics and tentative plan
4 Mandatory Assignments
5 People

Advanced Seminar in Linear Logic, Spring 2009

This course discusses linear logic, categorical models, type theoretic models, and proof theoretic. With this course we would like to gain a deeper understanding about fragments of linear logic, and their properties.

Practical and administrative matters

Lectures: Thursday 10:00-12:00 2A18.
The Monday lectures are 10:00-12:00 4A14.
The course period is 14 weeks (7.5 ects).
Students are expected to give lectures.
Master level students will take a pass/fail oral exam.

Topics and tentative plan

Below is a tentative plan.

Week	Date	Teacher	Topic	Materials	Labs
6	Thu 05 Feb	CS	Introduction to Linear Logic	Linear Intuitionistic Natural Deduction Frank Pfenning Course notes, pages 9-26
7	Thu 12 Feb	CS	Cut Eliminiation	Linear Sequent Calculus Frank Pfenning Course notes, pages 45-53
8	Thu 19 Feb	TBN	Focusing	Focusing Frank Pfenning Course notes, pages 67-75 A Logical Characterization of Forward and Backward Chaining in the Inverse Method Kaustuv Chaudhuri, Frank Pfenning, Greg Price, JAR, pages 133-150.
9	Thu 26 Feb	TBN, CS	Focusing, Classical Linear Logic	Linear Logic Jean-Yves Girard Theoretical Computer Science, 50:1-102, 1987.
10	Thu 05 Mar	CS	Linear Contextual Modal Type Theory	Linear Contextual Modal Type Theory Anders Schack-Nielsen and Carsten Schürmann, Draft.
11	Mon 09 Mar	REM	DILL as a metalanguage for domain theory	Dual intuitionistic linear logic Andrew Barber A Term Calculus for Intuitionistic Linear Logic Benton, Bierman, de Paiva and Hyland
12	Thu 12 Mar	KS	Domain theory and parametric polymorphism	Linear Abadi and Plotkin Logic Birkedal, Møgelberg and Petersen
13	Mon 30 Mar	REM	Categorical models of classical linear logic	Linear logic, *-autonomous categories and cofree coalgebras RAG Seely
14	Thu 02 Apr	REM	CBV and CBN interpretations into linear logic	Call-by-value, call-by-name, call-by-need and the linear lambda calculus Maraist, Odersky, Turner and Wadler Secondary reading Linear logic, Monads and the lambda calculus Benton and Wadler
16	Thu 16 Apr	REM	Enriched effect calculus	Enriching an Effect Calculus with Linear Types Egger, Møgelberg and Simpson
17	Thu 23 Apr	AB	Proof nets for multiplicative linear logic	Proof nets and the identity of proofs. Lutz Straßburger. INRIA RR 6013 (2006). Pages 1-10, 17-23, 33-34, 39-44.
18	Thu 30 Apr	SD	Introduction to games and full completeness	Is Game Semantics Necessary?. Andreas Blass. CSL 1993: 66-77. Mostly background and intuition. Should be an easy read. Games and Full Completeness for Multiplicative Linear Logic. Samson Abramsky and Radha Jagadeesan. Journal of Symbolic Logic 59(2):543-574 (1994). Read pages 543-554. The dual comment applies.
19	Thu 07 May	SD	Fully complete game model for MLL+MIX	Games and Full Completeness for Multiplicative Linear Logic. Samson Abramsky and Radha Jagadeesan. Journal of Symbolic Logic 59(2):543-574 (1994). Read pages 559-565.
20	Mon 11 May	SD	Higher-order Acyclic Graphs	Higher-Order Contexts via Games and the Int-construction (Extended Abstract). Lars Birkedal, Mikkel Bundgaard, Søren Debois, Davide Grohmann, and Thomas Hildebrandt. Submitted for publication. Secondary reading: Games & higher-order linear dataflow. Lars Birkedal, Søren Debois, and Thomas Hildebrandt.

Mandatory Assignments

Tentative Plan:

1.
2.
3.
4.
5.

People

(REM) Rasmus Ejlers Møgelberg
(SD) Søren Debois
(AB) Alexandre Buisse
(AF) Andrzej Filinski
(AS) Anders Starcke
(ASN) Anders Schack-Nielsen
(CS) Carsten Schürmann
(KS) Kasper Svendsen
(TBN) Taus Brock-Nannestad
(LN) Lasse Nielsen

Retrieved from "http://www.itu.dk/research/pls/wiki/index.php/ASLL-09"

Views

Personal tools

Log in

PLS

Wiki Navigation

Search

Toolbox