General Information

This is a research seminar, not a lecture course. Lectures will be organized around the discussion of one or more esearch papers taken from the conference proceedings and journals in the area of programming languages, logic, and type theory. You will be expected to read each paper covered and be prepared to discuss it in class. To facillitate the discussion, you are expected to post on WebCT prior to the class two positive and two negative aspects of the paper together with a question.

In addition, you will be required to lead 3 in-class discussion(s). Each presentation must be accompanied in advance by typeset lecture slides in either Powerpoint or LaTeX slide format and you must send a pdf-file containing the slides to the instructor prior to class. The presenter's slides will be posted on the course web site for future reference. The presenter is responsible for presenting a summary and a critical analysis of the paper(s) assigned to her (45 min), and to lead discussion (30min). The audience for a given paper is required to read the relevant papers in advance as preparation for the presentation.

The papers listed below represent an initial sample of the material we will cover in this class. It is to be expected that further reading will be required.

The practical component of the course will consist of a two-part project. In the first part, you will use existing dependently-typed programming language or proof assistant to assess its usability and power. An intermediate report is due in mid-October which will be reviewed by your peers. In the second part, you will design and implement a tool or technique which improves an existing programming/proof environment or tests its usability for a novel application. Your final report should take into account the comments you received during the first round and incorporate them. Your results and experiences will be presented to the class during a workshop.

There will also be a final exam consisting of essay questions requiring a synthesis of some or all of the papers covered in the course.

Please note that some of the links below will not work yet.

Schedule

Date

Lecture

Notes


Thu

Sep 1

Overview

Ch 2: Dependent types, Advanced Topics in Types and Programming Languages, B. Pierce


Tue

Sep 6

Dependent types cont.

Ch 2: Dependent types, Advanced Topics in Types and Programming Languages, B. Pierce

Thu

Sep 8

How to read a paper


Tue

Sep 13

Languages of the future

Francisco Ferreira

Thu

Sep 15

Dependently typed programming

Andrew Cave


Tue

Sep 20

DML

Ian Clement

Thu

Sep 22

Termination via dependent types

David Thibodeau


Tue

Sep 27

Sized types

  • MiniAgda: Integrating Sized and Dependent Types., Andreas Abel, Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR'10), pages 14-28, Electronic Proceedings in Theoretical Computer Science (EPTCS) vol 43, 2010.
  • Termination checking with types., Andreas Abel, RAIRO -- Theoretical Informatics and Applications, Special Issue: Fixed Points in Computer Science (FICS'03), vol 38(4): pages 277-319. 2004.

Costin Badescu

Thu

Sep 29

Programming with Coq

  • Position Paper: Thoughts on Programming with Proof Assistants, Adam Chlipala. Programming Languages meets Program Verification Workshop (PLPV'06). Electronic. Notes Theoretical Computer Science. 174, 7 (June 2007), pages 17-21. 2007
  • Program-ing Finger Trees in Coq, Matthieu Sozeau, In ACM SIGPLAN International Conference on Functional Programming (ICFP'07). pp.13--24, ACM Press, 2007.

Olivier Savary Belanger


Tue

Oct 4

Cayenne

Ian Clement

Thu

Oct 6

  • Dependent types and program equivalence.,Limin Jia, Jianzhou Zhao, Vilhelm Sjoberg, and Stephanie Weirich. In 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '10). pages 275-286,2010.

Francisco Ferreira


Tue

Oct 11

Proof certificates

  • Communicating and trusting proofs: The case for broad spectrum proof certificates. Dale Miller
  • A proposal for broad spectrum proof certificates. Dale Miller. First International Conference on Certified Proofs and Programs (CPP'11), to appear.
  • Efficient Representation and Validation of Proofs. George C. Necula, Peter Lee. In Proceedings of the 13th Annual symposium on Logic in Computer Science, Indianapolis, 1998.

David Thibodeau

Thu

Oct 13

No class; invited lecture by Dale Miller on Friday.


Tue

Oct 18

Logical frameworks

  • Logical Frameworks - Introduction, Frank Pfenning, In H. Schwichtenberg and R. Steinbrüggen, editors, Proof and System-Reliability, volume 62 of NATO Science Series II, pages 137-166. Kluwer Academic Publishers, 2002. Lecture notes from the Marktoberdorf Summer School, July 2001.
  • System Description: Twelf - A Meta-Logical Framework for Deductive Systems., In Harald Ganzinger, editor, 16th International Conference on Automated Deduction (CADE'99), pages 202-206, Lecture Notes in Computer Science (LNCS 1632), Springer, 1999.
  • Logical Frameworks, Frank Pfenning, In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, chapter 17, pages 1063-1147. Elsevier Science and MIT Press, 2001.

Brigitte Pientka

Thu

Oct 20

    Reading see the one from Oct 20

Brigitte Pientka


Tue

Oct 25

Beluga

Brigitte Pientka

Thu

Oct 27

Delphin

Brigitte Pientka


Tue

Nov 1

Other approaches to binding

  • A universe of binding and computation. Daniel R. Licata and Robert Harper. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09). pages 123-134, ACM, 2009.
  • Nameless, painless. Nicolas Pouillard. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP '11). ACM, 2011.

Andrew Cave

Thu

Nov 3

Programming theorem provers

Costin Badescu


Tue

Nov 8

Combining programming and proving

David Thibodeau

Thu

Nov 10

Proof irrelevance

  • Intensionality, extensionality, and proof irrelevance in modal type theory. Frank Pfenning. In J. Halpern, editor, Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS'01), pages 221-230, IEEE Computer Society Press. 2001

Olivier Savary Belanger


Tue

Nov 15

Proof-carrying Code

  • Proof-carrying code. George C. Necula. w In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '97). pages 106-119. ACM, 1997.

Costin Badescu

Thu

Nov 17

Class cancelled


Tue

Nov 22

Proof-carrying authorization

  • A General and Flexible Access-Control System for the Web. Lujo Bauer, Michael A. Schneider, and Edward W. Felten. In Proceedings of the 11th USENIX Security Symposium, Dan Boneh (Ed.). pages 93-108. USENIX Association, 2002.
  • A Proof-carrying File System. Deepak Garg and Frank Pfenning. In Proceedings of the 2010 IEEE Symposium on Security and Privacy (SP '10). pages 349-364.IEEE Computer Society, Washington, DC, USA. 2010.

Ian Clement

Thu

Nov 24

Extensible proof-checking

  • Static and User-Extensible Proof Checking. Antonis Stampoulis and Zhong Shao. In Proc. 39th ACM Symposium on Principles of Programming Languages (POPL'12), Philadelphia, Pennsylvania, pages (to appear), January 2012. ©2012 ACM.

Olivier Savary Belanger


Tue

Nov 29

Homotopy Type Theory (Introduction)

  • Thorsten Altenkirch. A short history of equality. (slide)
  • Dan Doel. Homotopy and Directed Type Theory: A Sample. (slides)
  • Dan Licata. Just Kidding: Understanding Identity Elimination in Homotopy Type Theory.(blog post)
  • Daniel R. Licata and Robert Harper. Canonicity for 2-Dimensional Type Theory.(paper accepted at POPL-2012, gives a good introduction,motivation, and conclusion, but gets technical in the middle)

Andrew Cave

Thu

Dec 1

Workshop day