15-819 Advanced Topics in the Theory of Programming Languages

Course Information

Time:	Mon-Wed 3:00-4:30
Room:	4615A Wean Hall
Instructor:	Robert Harper

Description

This is a graduate reading course on the theory of programming languages. The goal of the course is to introduce some of the fundamental tools used in research in the area.

Participation in this course consists of presenting a body of research in the area in the form of one or two lectures and associated course notes.

Topics

The emphasis will be on proof-theoretic and type-theoretic methods in programming languages. The following topics will be considered:

• Judgements, Rules, Evidence
• Proofs and Types
• Simple Types
• Polymorphic Types
• Dependent Types
• Operational Methods for PCF and Extensions
• Normalization by Evaluation
• Focusing and Polarity

Please see the readings for references for the material in this course.

Schedule

Date		Presenter	Topic	References
Sep	8	Harper	The Logic of Judgements	Simple Consequence Relations, Practical Foundations for Programming Languages.
	10	Harper	The Logic of Judgements	On the Meanings of the Logical Constants..., A Framework for Defining Logics.
	15	Harper	Curry-Howard Correspondence	Proofs and Types
	17	Harper	Proof Equivalence	Proofs and Types, Confluent Reduction ...
	22	Harper	Logical Relations: Strong Normalization	Proofs and Types, Metamathematical Investigations ...
	24	Harper	Logical Relations: Equivalence and Canonization	Proofs and Types, Metamathematical Investigations ...
	29	Harper	Goedel's System T	Proofs and Types, Combinators, λ-Terms, and Proof Theory
Oct	1	Harper	Inductive and Coinductive Types	Inductive Types and Type Constraints in the Second-Order Lambda Calculus
	6	Harper	Inductive and Coinductive Types	Inductive Types and Type Constraints in the Second-Order Lambda Calculus
	8	Harper	Categorical Type Theory; Initial Algebras and Final Coalgebras	Categorical Logic and Type Theory , Mendler-Style Inductive Types, Categorically
	13	Harper	Girard's System F	Proofs and Types
	15	Harper	Girard's Method: Termination for System F	Proofs and Types
	20	(No Class)
	22	(No Class)
	27	Harper	Definability of Initial Algebras in System F	Proofs and Types, On Functors Expressible in the Polymorphic Typed Lambda Calculus
	29	Harper	Observational and Logical Equivalence for System T	Practical Foundations for Programming Languages , Typed Operational Reasoning
Nov	3	Harper	Observational and Logical Equivalence for System T	Practical Foundations for Programming Languages , Typed Operational Reasoning
	5	Harper	Relational Parametricity for System F	Practical Foundations for Programming Languages , Outline of a Proof Theory of Parametricity , Theorems for Free!
	10	Harper	Relational Parametricity for System F	Practical Foundations for Programming Languages , Outline of a Proof Theory of Parametricity , Theorems for Free!
	12	Harper	Observational Equivalence for PCF	Practical Foundations for Programming Languages , Operational Semantics and Program Equivalence, Techniques for Contextual Equivalence in Higher-Order, Typed Languages
	17	Harper	Observational Equivalence for PCF	Practical Foundations for Programming Languages , Operational Semantics and Program Equivalence, Techniques for Contextual Equivalence in Higher-Order, Typed Languages
	19	(no class)
	24	Harper	Dependent Types	On Equivalence and Canonical Forms in the LF Type Theory
	26	(no class)	(Thanksgiving break)
Dec	1	Harper	Dependent Types	On Equivalence and Canonical Forms in the LF Type Theory
	3	Harper	Singleton Types	Extensional Equivalence and Singleton Types.

Robert Harper

Last modified: Mon Nov 24 14:45:32 EST 2008