CS 629 Advanced Topics in Programming Language Research (Spring 2004)

CS 629 Advanced Topics in Programming Language Research

(Spring 2004)

Course Info

In this seminar we will discuss advanced topics in the design and semantics of high-level programming languages, with emphasis on techniques and tools for specifying and proving properties of programs. The seminar will be organized as a sequence of mini-courses, covering topics including but not limited to:

advanced type systems, including:
- higher-order polymorphic type systems
- pure type systems and logics
- logic-based type systems
automated proof systems, including:
- logical frameworks
- proof assistants
- metaprogramming for logical frameworks
advanced models for computational specifications, including:
- continuations
- monads and monad transformers
- arrows

The mini-courses will comprise about 3/4 of the overall course. In the remaining time, students will be expected to present papers on these or related topics.

Pre-requisites:

CS429 or CS430 (or both). Undergraduates may take the course with permission of the instructors.

Time and place:

WF 10-11:30 in 400 AKW

Instructors:

	Office	Office Hours
Paul Hudak	308 AKW	TBA
Carsten Schürmann	312 AKW	drop by
Valery Trifonov	304 AKW	drop by

Texts

Benjamin C. Pierce, Scott Dietzen, and Spiro Michaylov. Programming in Higher-order Typed Lambda-Calculi. Tech Report CMU-CS-89-111.
Local copies: PS | 2-up PS (for printing)
Henk Barendregt. Introduction to generalized type systems. JFP 1 (2) 125-154, 1991.
Henk Barendregt, Herman Geuvers. Proof assistants using Dependent Type Systems. Chapter 3 of Handbook of Automated Reasoning, Elsevier 2001.
Herman Geuvers. A short and flexible proof of Strong Normalization for the Calculus of Constructions. In TYPES'94, LNCS 996, pp. 14-38, Springer.
Local copies: PS | 2-up PS (for printing)
Per Martin-Löf. On the meaning of the logical constants and the justifications of the logical laws. Nordic J. of Philosophical Logic 1 (1), pp. 11-60.
Local copies: PS | 2-up PS (for printing)
Frank Pfenning. Computation and Deduction, draft of April 2, 1997. 312 pages.
Local copies: PS | 2-up PS (for printing)
Frank Pfenning. Logical Frameworks. Chapter 17 of Handbook of Automated Reasoning, pp. 1063-1147. ©Elsevier 2001.
Local copies: PS | 2-up PS (for printing)
Philip Wadler. Monads for functional programming. August 2001, 31 pages.
Local copy: PDF
Sheng Liang and Paul Hudak. Modular Monadic Semantics. March 1998, 56 pages.
Local copy: PDF

Assignments

Due Monday, Feb 23, 2004: Assignment 1

Code

Representing propositional logic in Twelf: sources.cfg, prop-calc.elf, ndclass.elf, thm1.elf, thm2.elf, thm3.elf
Representing propositional logic in Coq: propcalc.v.
(Get Coq here; this code was tested with version 7.4. One way to run it is to execute coqtop and enter Load "propcalc.v". at the prompt.)

http://flint.cs.yale.edu/trifonov/cs629/
Last updated 2004-04-13
Valery Trifonov