CSCI 384 Fall 2021

Foundations of Programming Languages

                                                               “Giving lambda its legs since the year 2000.”

……………………. . . . . . . . . . . . . .

This course examines the means for expression and execution of computer programs, focusing on programming systems geared towards checking programs. We’ll develop our own programming languages, and we’ll write parsers, interpreters, and checkers for the languages that we invent. Our goal is to go beyond languages like Python and C++ and learn approaches to study a wider variety of programming languages.

We first examine functional programming languages. like Haskell and dialects of ML, because of their sophisticated type systems. These require us to look at Church’s lambda calculus which serves as their foundation. These languages’ type systems are tied very closely to mathematical logic. We will study this correspondence and how it relates to mathematical proof, seeing proof as a kind of programming.

We’ll finish by modeling features found in C-like languages, especially side-effecting statements and exceptions, studying the use of monads, continuations, and control operations in functional programming languages. We’ll use the Agda programming language to express and prove properties of programs. We look more generally at these proof assistants and their dependant type systems.

Prerequisites: MATH 112 or 113; you must be familiar with making mathematical arguments and giving mathematical proofs. CSCI 221 or the equivalent

Meets: 3-4:20MW in Physics 240A.
Instructor: Jim Fix jimfix@reed.edu
Office: Library 314
Office Hours: 10-11TuW, 1-2Tu

……………………. . . . . . . . . . . . . . . . .

Course Schedule

Week 01: Syntactic specification and analysis.
• Homework 1: grammars; OCaml-lite
Week 02: Grammars and ambiguity.
• Homework 2: trees.
   => my solution Week 03: Recursive-descent parsing. Standard ML.
• Homework 3: parsing.
• the syntax of SML
Week 04: algebraic datatypes; interpretation.
• some sample datatype code
• syntax for datatypes
• Homework 4: SML.
Week 05: big-step operational semantics. closures
Week 06: Church’s lambda calculus.
Week 07: beta reduction. Church encodings.
• Homework 5: MiniML interpreter
BREAK
Week 08: the Y combinator.
• Homework 6: lambda reducer
Week 09: Types.
Week 10: Unification and type inference.
Week 11: Curry-Howard.
• Homework 7: typed MiniML
Week 12: Control operators. Continuations.
• notes on types and control
Week 13: Classical logic and CPS. Monads.
• Homework 8: stacks and proofs.
Week 14: Logic and langage foundations in Agda.

……………………. . . . . . . . . . . . . . . . .

Responsibilities and Evaluation

There will be regular homework assignments based on the lecture and reading material, roughly every week. These typically involve writing tricky programs in, or designing features of, the language systems we cover in lecture. Thus, they’ll be a mix of written work and programming work. In addition, there will be several projects where you will implement some component of a programming language system, including:

  • a recursive-descent parser
  • several program interpreters
  • a type reconstruction engine
  • a lambda calculus reduction engine

……………………. . . . . . . . . . . . . . . . .

Learning Outcomes

Students will be able to
• model the syntax of a programming language using a (context-free) grammar
• write code that parses a sequence of tokens into an abstract syntax tree (AST)
• write interpreter code that executes a program, construed as an AST
• write moderately complex code in a (purely) functional programming language (e.g. Standard ML, Haskell), including code that treats a program as data
• devise inference rules specifying the semantics of a programming language, both its “static” type system and its programs’ “dynamic” evaluation
• write code for (Hindley-Milner) type reconstruction and type term unification
• express computations in Church’s lambda calculus; explain its relevance to modern programming languages
• express the semantics of control operations using continuations
• write purely functional code with side-effects using monads
• explain the relationship between proofs/logic and programs/types
• write proofs/code in a dependently typed proof assistant (e.g. Agda, Coq)

……………………. . . . . . . . . . . . . . . . .

Bottom