Differences between revisions 1 and 63 (spanning 62 versions)
Revision 1 as of 2012-10-11 14:56:39
Size: 17
Editor: dreyer
Comment:
Revision 63 as of 2013-02-02 19:20:15
Size: 7899
Editor: dreyer
Comment:
Deletions are marked like this. Additions are marked like this.
Line 1: Line 1:
This is a stub. = Parametricity and Modular Reasoning =

'''Instructor:''' [[http://www.mpi-sws.org/~dreyer|Derek Dreyer]]

'''TA/Scribe:''' [[http://www.mpi-sws.org/~swasey|Dave Swasey]]

'''Meeting time:''' Tue, Thu @ 2:00-4:00 PM

'''Place:''' Campus E1.5, Room 029 (videocast to KL)

== Abstract ==

Abstract data types (ADTs) and other facilities for information hiding
in programming languages (e.g. private fields, local variables) are
widely considered to be crucial for supporting data abstraction and
modularity, but what does that actually buy us in terms of reasoning
about our code? As it turns out, it buys us a great deal, but
formalizing what it buys us, especially in the context of modern
programming languages, is quite tricky.

The formal essence of data abstraction was first characterized by John
Reynolds in a landmark 1983 paper, "Types, Abstraction and Parametric
Polymorphism", in which he introduced the concept of "relational
parametricity" via his "abstraction theorem". The abstraction theorem
formally establishes that the behavior of clients of an ADT must be
unaffected by changes to the internal representation of the ADT that
are preserved by its operations. However, Reynolds's original work
only concerned pure System F, the polymorphic lambda-calculus, and
there have since been decades of work on extending and generalizing
his results to richer, more realistic languages supporting a host of
computational effects.

In this course, we will start with Reynolds's work and build
progressively toward semantic models of modern languages, such as
Kripke logical relations and bisimulations models, which support very
subtle and sophisticated forms of modular reasoning. To keep the
formal material of the course in a unified framework, we will focus on
models of data abstraction based on *operational* semantics, in the
tradition of the work of Andrew Pitts.

As a basic prerequisite, students should be familiar with standard
operational techniques, such as proofs by induction over operational
semantics and type systems, which are covered in Pierce's TAPL book
and Harper's PFPL book, among other sources. The grade will be based
on homework assignments, student presentations on assigned papers, and
class participation.

Along the way, we will explore a number of the following topics,
possibly among others:

 * Proving termination/normalization of System F (Girard's method, "unary logical relations")
 * Relational parametricity (Reynolds's abstraction theorem, "binary logical relations")
 * Representation independence as an application of parametricity (Mitchell)
 * Using parametricity to show definability of types by Church encodings
 * "Free" theorems (Wadler) and applications to fusion optimizations (Johann)
 * Relational parametricity and "units of measure" (Kennedy)
 * Supporting recursion and context-sensitive semantics by "TT-closure" (Pitts)
 * Supporting local invariants on first-order state via "Kripke logical relations" (Pitts-Stark)
 * Supporting recursive types and higher-order state by "step-indexed" Kripke logical relations (Appel-McAllester, Ahmed)
 * Transitional invariants (Dreyer et al.)
 * Environmental bisimulations (Sumii et al.)
 * Parametric bisimulations (Hur et al.)
 * Logical relations for concurrency (Turon et al.)

== Schedule ==

|| '''Date and time''' || '''Topic''' || '''Presenter''' || '''Scribe''' || '''Other Files''' ||
|| Tue, 2012-10-16 || Introduction || Derek || [[attachment:20121016.pdf|Dave]] || ||
|| Thu, 2012-10-18 || System F; Girard's method for proving termination || Derek || [[attachment:20121018.pdf|Dave]] || [[attachment:girard.pdf|Girard, Lafont, Taylor (1990)]] <<BR>> [[attachment:gallier.pdf|Gallier (1990)]] ||
|| Tue, 2012-10-23 || Unary parametricity (applications of Girard's method) || Derek || [[attachment:20121023.pdf|Dave]] || [[attachment:swasey-notes1.pdf|Dave's writeup of Derek's FTLR proof]] ||
|| Thu, 2012-10-25 || '''''Class cancelled (Derek out of town)''''' || || ||
|| Tue, 2012-10-30 || Relational parametricity (Reynolds) || Derek || [[attachment:20121030.pdf|Dave]] || [[attachment:reynolds.pdf|Reynolds (1983)]] <<BR>> '''[[attachment:hw1.pdf|Homework #1]]''' ||
|| Thu, 2012-11-1 || '''''No class (All Saints' Day)''''' || || ||
|| Tue, 2012-11-6 || Definability of types by Church encodings || Derek || [[attachment:20121106.pdf|Dave]] || [[attachment:plotkin-abadi.pdf|Plotkin, Abadi (1993)]] <<BR>> [[attachment:birkedal-mogelberg.pdf|Birkedal, Møgelberg (2005)]] <<BR>> '''[[attachment:hw2.pdf|Homework #2]]''' ||
|| Thu, 2012-11-8 || Free theorems; short cut fusion || Derek || [[attachment:20121108.pdf|Dave]] || [[attachment:wadler.pdf|Wadler (1989)]] <<BR>> [[attachment:gill.pdf|Gill, Launchbury, Peyton Jones (1993)]] <<BR>> [[attachment:johann.pdf|Johann (2003)]] <<BR>> [[attachment:johann-popl04.pdf|Johann (2004)]] ||
|| Tue, 2012-11-13 || Representation independence || Derek || [[attachment:20121113.pdf|Dave]] || [[attachment:mitchell-plotkin.pdf|Mitchell, Plotkin (1988)]] <<BR>> [[attachment:mitchell.pdf|Mitchell (1986)]] <<BR>> [[attachment:pitts-attapl.pdf|Pitts' ATTAPL chapter (2005)]] ||
|| Thu, 2012-11-15 || Recursion and admissibility || Derek || [[attachment:20121115.pdf|Dave]] || [[attachment:pitts-densem-notes.pdf|Pitts' lecture notes on denotational semantics]] ||
|| Tue, 2012-11-20 || TT-closure || Derek || [[attachment:20121120.pdf|Dave]] || [[attachment:pitts-attapl.pdf|Pitts' ATTAPL chapter (2005)]] <<BR>> '''[[attachment:hw3.pdf|Homework #3]]''' ||
|| Thu, 2012-11-22 || TT-closure (continued) || Derek || [[attachment:20121122.pdf|Dave]] || ||
|| Tue, 2012-11-27 || TT-closure (continued); Completeness and CIU-equivalence || Derek || [[attachment:20121127.pdf|Dave]] || '''[[attachment:hw4.pdf|Homework #4]]''' ||
|| Thu, 2012-11-29 || Unwinding Theorem; Contextual equivalence at existential types || Derek || [[attachment:20121129.pdf|Dave]] || ||
|| Tue, 2012-12-4 || Positive recursive types || Derek || [[attachment:20121204.pdf|Dave]] || ||
|| Thu, 2012-12-6 || First-class continuations || Derek || [[attachment:20121206.pdf|Dave]] || [[attachment:dreyer-neis-birkedal.pdf|Dreyer, Neis, Birkedal (2010-12)]] ||
|| Tue, 2012-12-11 || General recursive types, step-indexing || Derek || [[attachment:20121211.pdf|Dave]] || [[attachment:appel-mcallester.pdf|Appel, McAllester (2001)]] <<BR>> [[attachment:ahmed-2006.pdf|Ahmed (2006)]] <<BR>> '''[[attachment:hw5.pdf|Homework #5]]''' ||
|| Thu, 2012-12-13 || General recursive types, step-indexing (continued) || Derek || [[attachment:20121213.pdf|Dave]] || ||
|| Tue, 2012-12-18 || Combining step-indexing and TT-closure || Derek || [[attachment:20121218.pdf|Dave]] || ||
|| Thu, 2012-12-20 || Proving Støvring and Lassen, LSLR paper || Derek || [[attachment:20121220.pdf|Dave]] || [[attachment:plotkin-abadi.pdf|Plotkin, Abadi (1993)]] <<BR>> [[attachment:dreyer-ahmed-birkedal.pdf|Dreyer, Ahmed, Birkedal (2009-11)]] ||
|| Tue, 2013-01-08 || First-order state and Kripke-logical relations || Derek || [[attachment:20130108.pdf|Dave]] || [[attachment:pitts-stark.pdf|Pitts, Stark (1998)]] ||
|| Thu, 2013-01-10 || First-order state (continued) || Derek || [[attachment:20130110.pdf|Dave]] || ||
|| Thu, 2013-01-17 || Transitional invariants || Derek || [[attachment:20130117.pdf|Dave]] || [[attachment:dreyer-neis-birkedal.pdf|Dreyer, Neis, Birkedal (2010-12)]] <<BR>> [[attachment:ahmed-dreyer-rossberg.pdf|Ahmed, Dreyer, Rossberg (2009)]] ||
|| Tue, 2013-01-29 || Higher-order state || Derek || [[attachment:20130129.pdf|Dave]] || [[attachment:dreyer-neis-birkedal.pdf|Dreyer, Neis, Birkedal (2010-12)]] ||
|| Thu, 2013-01-31 || The JFP Paper || Derek || [[attachment:20130131.pdf|Dave]] || [[attachment:dreyer-neis-birkedal.pdf|Dreyer, Neis, Birkedal (2010-12)]] ||

Parametricity and Modular Reasoning

Instructor: Derek Dreyer

TA/Scribe: Dave Swasey

Meeting time: Tue, Thu @ 2:00-4:00 PM

Place: Campus E1.5, Room 029 (videocast to KL)

Abstract

Abstract data types (ADTs) and other facilities for information hiding in programming languages (e.g. private fields, local variables) are widely considered to be crucial for supporting data abstraction and modularity, but what does that actually buy us in terms of reasoning about our code? As it turns out, it buys us a great deal, but formalizing what it buys us, especially in the context of modern programming languages, is quite tricky.

The formal essence of data abstraction was first characterized by John Reynolds in a landmark 1983 paper, "Types, Abstraction and Parametric Polymorphism", in which he introduced the concept of "relational parametricity" via his "abstraction theorem". The abstraction theorem formally establishes that the behavior of clients of an ADT must be unaffected by changes to the internal representation of the ADT that are preserved by its operations. However, Reynolds's original work only concerned pure System F, the polymorphic lambda-calculus, and there have since been decades of work on extending and generalizing his results to richer, more realistic languages supporting a host of computational effects.

In this course, we will start with Reynolds's work and build progressively toward semantic models of modern languages, such as Kripke logical relations and bisimulations models, which support very subtle and sophisticated forms of modular reasoning. To keep the formal material of the course in a unified framework, we will focus on models of data abstraction based on *operational* semantics, in the tradition of the work of Andrew Pitts.

As a basic prerequisite, students should be familiar with standard operational techniques, such as proofs by induction over operational semantics and type systems, which are covered in Pierce's TAPL book and Harper's PFPL book, among other sources. The grade will be based on homework assignments, student presentations on assigned papers, and class participation.

Along the way, we will explore a number of the following topics, possibly among others:

  • Proving termination/normalization of System F (Girard's method, "unary logical relations")
  • Relational parametricity (Reynolds's abstraction theorem, "binary logical relations")
  • Representation independence as an application of parametricity (Mitchell)
  • Using parametricity to show definability of types by Church encodings
  • "Free" theorems (Wadler) and applications to fusion optimizations (Johann)
  • Relational parametricity and "units of measure" (Kennedy)
  • Supporting recursion and context-sensitive semantics by "TT-closure" (Pitts)
  • Supporting local invariants on first-order state via "Kripke logical relations" (Pitts-Stark)
  • Supporting recursive types and higher-order state by "step-indexed" Kripke logical relations (Appel-McAllester, Ahmed)

  • Transitional invariants (Dreyer et al.)
  • Environmental bisimulations (Sumii et al.)
  • Parametric bisimulations (Hur et al.)
  • Logical relations for concurrency (Turon et al.)

Schedule

Date and time

Topic

Presenter

Scribe

Other Files

Tue, 2012-10-16

Introduction

Derek

Dave

Thu, 2012-10-18

System F; Girard's method for proving termination

Derek

Dave

Girard, Lafont, Taylor (1990)
Gallier (1990)

Tue, 2012-10-23

Unary parametricity (applications of Girard's method)

Derek

Dave

Dave's writeup of Derek's FTLR proof

Thu, 2012-10-25

Class cancelled (Derek out of town)

Tue, 2012-10-30

Relational parametricity (Reynolds)

Derek

Dave

Reynolds (1983)
Homework #1

Thu, 2012-11-1

No class (All Saints' Day)

Tue, 2012-11-6

Definability of types by Church encodings

Derek

Dave

Plotkin, Abadi (1993)
Birkedal, Møgelberg (2005)
Homework #2

Thu, 2012-11-8

Free theorems; short cut fusion

Derek

Dave

Wadler (1989)
Gill, Launchbury, Peyton Jones (1993)
Johann (2003)
Johann (2004)

Tue, 2012-11-13

Representation independence

Derek

Dave

Mitchell, Plotkin (1988)
Mitchell (1986)
Pitts' ATTAPL chapter (2005)

Thu, 2012-11-15

Recursion and admissibility

Derek

Dave

Pitts' lecture notes on denotational semantics

Tue, 2012-11-20

TT-closure

Derek

Dave

Pitts' ATTAPL chapter (2005)
Homework #3

Thu, 2012-11-22

TT-closure (continued)

Derek

Dave

Tue, 2012-11-27

TT-closure (continued); Completeness and CIU-equivalence

Derek

Dave

Homework #4

Thu, 2012-11-29

Unwinding Theorem; Contextual equivalence at existential types

Derek

Dave

Tue, 2012-12-4

Positive recursive types

Derek

Dave

Thu, 2012-12-6

First-class continuations

Derek

Dave

Dreyer, Neis, Birkedal (2010-12)

Tue, 2012-12-11

General recursive types, step-indexing

Derek

Dave

Appel, McAllester (2001)
Ahmed (2006)
Homework #5

Thu, 2012-12-13

General recursive types, step-indexing (continued)

Derek

Dave

Tue, 2012-12-18

Combining step-indexing and TT-closure

Derek

Dave

Thu, 2012-12-20

Proving Støvring and Lassen, LSLR paper

Derek

Dave

Plotkin, Abadi (1993)
Dreyer, Ahmed, Birkedal (2009-11)

Tue, 2013-01-08

First-order state and Kripke-logical relations

Derek

Dave

Pitts, Stark (1998)

Thu, 2013-01-10

First-order state (continued)

Derek

Dave

Thu, 2013-01-17

Transitional invariants

Derek

Dave

Dreyer, Neis, Birkedal (2010-12)
Ahmed, Dreyer, Rossberg (2009)

Tue, 2013-01-29

Higher-order state

Derek

Dave

Dreyer, Neis, Birkedal (2010-12)

Thu, 2013-01-31

The JFP Paper

Derek

Dave

Dreyer, Neis, Birkedal (2010-12)

paramore (last edited 2013-03-03 23:20:23 by dreyer)