CSCE-604 Programming Language Design (Fall 2014)

Course Essentials

Course CSCE 604 – Programming Language Design, 12:45 pm–02:00 pm, HRBB 113
Instructor Jaakko Järvi
Course pages http://courses.cse.tamu.edu/jarvi/2014/CSCE-604
Contact jarvi@cse.tamu.edu
Office hours By appointment (my office is 416)
Teaching Assistant Plamen Ivanov (flame09@neo.tamu.edu), office hours: TBA

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.

News

Schedule and material

Date Topic  
Tue, Sep 2 Class setup (pdf); Specifying Syntax and Semantics (pdf)  
Thu, Sep 4 Structural Induction.  
Tue, Sep 9 Small step semantics (pdf)  
Thu, Sep 11 Intro to Haskell (pdf)  
Tue, Sep 16 Guest lecture: Functional Reactive Programming, Jason Wilkins  
Thu, Sep 18 Intro to Haskell continued  
Tue, Sep 23 Simple types (pdf)  
Thu, Sep 25 Simple types  
Tue, Sep 30 Lambda calculus (pdf)  
Thu, Oct 2 Simply typed lambda calculus (pdf)  
Tue, Oct 7 Simply typed lambda calculus, extensions  
Thu, Oct 9 Monads (pdf, monad-code.tar)  
Tue, Oct 14 Monads  
Thu, Oct 16 Midterm  
Tue, Oct 21 Functional parsers (pdf, parsing.hs)  
Thu, Oct 23 Subtyping (pdf)  
Tue, Oct 28 Store and references (pdf)  
Thu, Oct 30 System F (pdf)  
Tue, Nov 4 System F  
Thu, Nov 6 Existential types  
Tue, Nov 11 Bounded quantification (pdf)  
Thu, Nov 13 FJ (notes)  
Tue, Nov 18 FJ, FGJ (notes)  
Thu, Nov 20 FGJ  
Tue, Nov 25 Curry-Howard correspondence (notes)  
Thu, Nov 27 No class — Thanksgiving  
Tue, Dec 2 Student project presentations  
Thu, Dec 4 Student project presentations  
Tue, Dec 9 Final exam  

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 being introduced; 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.

Assignments

Assignment 1. This LaTeX file may be useful, and this package is to build it. Answers Due on [2014-09-16 Tue]
Assignment 2. This Haskell file is a starting point. Answers Due on [2014-09-29 Mon]
Assignment 3. This Haskell file is a starting point. Lambda calculus reduction rules. LaTeX source in case it is useful Answers Due on [2014-10-13 Mon]
Assignment 4. This tar-ball gives a starting point.   Due on [2014-10-31 Fri]

Exams

Midterm exam is on Thursday, Oct 16th, 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
    • Maybe, but likely we will not make it that far: Section 13

Final exam is on Tuesday, Dec 9th, during regular class period. Material:

  • All class notes/slides
  • From Pierce:
    • Section 13
    • Subsections 15.1–15.5
    • Section 16
    • Section 19
    • Subsection 23.1–23.6 (read 23.8–23.9 too, it's good for you)
    • Section 24
    • Subsections 26.1–26.4
    • Subsections 28.1–28.3

Resources

Software

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 linux.cse.tamu.edu and compute.cse.tamu.edu 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:

ghci 

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: 2014-11-25 Tue 12:17

Emacs 24.4.1 (Org mode 8.2.10)

Validate