CSCE-604 Programming Language Design (Fall 2015)

Course Essentials

Course CSCE 604 — Programming Language Design, 08:00 – 09:15 am, O&M 206
Instructor Jaakko Järvi
Course pages
Office hours By appointment (my office is 416)

In a nutshell

Study in the design space of programming languages, covering language processing, formalisms to describe semantics of programming languages, important concepts found in current programming languages, and programming paradigms.

The syllabus can be found here.


Schedule and material

Date Topic  
Tue, Sep 1 Class setup (pdf); Specifying Syntax and Semantics (pdf)  
Thu, Sep 3 Specifying semantics  
Tue, Sep 8 Structural Induction; simple proofs about languages  
Thu, Sep 10 Small step semantics (pdf)  
Tue, Sep 15 Introduction to Haskell (pdf)  
Thu, Sep 17 Introduction to Haskell  
Tue, Sep 22 Intro to Haskell, simple types (pdf)  
Thu, Sep 24 Simple types  
Tue, Sep 29 Guest lecture: Jason Wilkins, Reactive Programming (pptx)  
Thu, Oct 1 Guest lecture: Jeff Huang  
Tue, Oct 6 Simple types  
Thu, Oct 8 Untyped lambda calculus (pdf)  
Tue, Oct 13 More on lambda calculus (code we discussed)  
Thu, Oct 15 Simply typed lambda calculus (pdf)  
Tue, Oct 20 Simply typed lambda calculus  
Thu, Oct 22 Extending lambda calculus, subtyping (pdf)  
Tue, Oct 27 Midterm exam  
Thu, Oct 29 Subtyping  
Tue, Nov 3 Midterm discussion  
Thu, Nov 5 About Haskell Monads (pdf)  
Tue, Nov 10 More on monads  
Thu, Nov 12 Typing store and references (pdf)  
Tue, Nov 17 System F (pdf)  
Thu, Nov 19 System F  
Tue, Nov 24    
Thu, Nov 26 No class — Thanksgiving  
Tue, Dec 1    
Thu, Dec 3    
Tue, Dec 8    

Note to a prospective student

Programming languages are an active research area, the goals of which include ever safer, more efficient, and expressive languages and programming environments. Results from recent programming language research are finding their way to main stream languages, both C# and Java have in the recent years been extended with generics, Java with wildcards, C++, Java, and C# have gotten lambda functions, C++ big changes to its template system; new interesting languages, such as Scala with advanced type systems are gaining popularity; languages that combine a theorem prover with a mainstream language have been introduced; new languages aimed primarily to concurrent programming, and new abstractions to existing languages to better support concurrent programming are being developed; and so forth. The list goes on. For a motivated student, this class is an opportunity to get involved in this exciting research area.

About the course

The primary text for the course is:

Benjamin C. Pierce: Types and Programming Languages

Not all of the book will be covered, and other material is used as well, but this book will be necessary to have.

The course aims to deepen understanding on the concepts and features of programming languages, and provide means to (formally) reason about languages and language features, to the extent to become able to appreciate current research and developments in the area of programming languages. Programming languages are a very large research area. Consequently, the course focus is on fundamental mechanisms rather than broadness. Not everything can be covered: the emphasis of the text is on static typing, type systems etc., which will comprise the main body of this course as well.

We start from Lambda calculus as the simplest model of a programming language and gradually extend it with language features. The basics that are covered include

  • Specifying semantics of programming languages
  • Necessary proof techniques for programming language research
  • Lambda calculus
  • Specifying type systems
  • Formal study of properties of type systems and languages (such as type safety)

Equipped with this basic skill set, we'll study more ambitious language constructs, such as:

  • Subtyping
  • Polymorphism and generics
  • Constrained generics (bounded quantification)
  • Other recent advances/questions in programming languages/type systems

A likely class project will be an in-depth study of some interesting language feature, type system, etc. that has had some recent interest in the programming language research community.


Information on projects found here.


Assignment 1. This LaTeX file may be useful, and this package is needed to build it. Answers Due on [2015-09-18 Fri]
Assignment 2. This Haskell file is a starting point. Answers Due on [2015-10-04 Sun]
Assignment 3. This Haskell file is a starting point. LaTeX source in case it is useful Answers not available yet Due on [2015-10-15 Thu]
Assignment 4. This tar-ball gives a starting point.   Due on [2015-11-29 Sun]


The midterm exam is on Tuesday, Oct 27th, during normal class hours. Reading for the exam:

  • All slides
  • All assignments
  • From Pierce:
    • Section 1
    • Section 2 if you feel you need that
    • Sections 3, 5, 8
    • Subsections 9.1–9.3
    • Subsections 11.1–11.4, 11.6–11.8



Many programming assignments will be done with Haskell, here are a few pointers to get you started:

Using GHC

A few other compilers exist, but we will use the Glasgow Haskell Compiler. It is installed on and servers.

An easy way to interact with GHC is to edit your document, say, Foo.hs in your favourite editor (== Emacs, with haskell-mode), and invoke the GHC interpreter in a shell window:


The most commonly used commands are

  • :l Foo to load the module Foo (from your file foo.hs)
  • :r to re-load the previously loaded module
  • :i x to inspect the value, type, … x
  • :t x to show the type of x
  • :q to quit the interpreter

The compiler is invoked, for example as:

ghc --make main.hs

The --make option determines automatically which modules need to be recompiled, so you don't have to write a Makefile yourself. (Also GHC's analysis of what need to be recompiled is more fine grained, thus faster).

Author: Jaakko Järvi

Created: 2015-11-19 Thu 19:13

Emacs 24.4.1 (Org mode 8.2.10)