PL II

Lecture Outline

This is the preliminary list of M/W lecture topics and readings. See the dateline for what we actually end up doing.

The M/W topics are primarily focused on higher-order and functional programming, following the pattern of PoPL I.

Friday is a paper reading day which will cover some recent papers as well as surveys of some topics we could not fit in the M/W days.

More Functional Programming in OCaml

To warm up let's cover some stuff that is more "PL I" but we didn't have the time to cover it there.

• Pipelining
• Folds and generalized folds
• OCaml modules and functors
• Generalized Abstract Data Types (GADTs) in OCaml

• Folds and Pipelining: Cornell CS, Functional Programming in OCaml: Folds
• GADT's: the OCaml manual chapter 8.11; Detecting use-cases for GADTs in OCaml by Mads Hartmann;

Transformations

• A-translation
• Closure Conversion
• Defunctionalization
• Continuation-passing style, CPS transformation, and exceptions encodings
• State-passing style and reader/writer threading
• Unifying transformations with the monad template
• Programming with monads and monad transformers

• Xavier Leroy, Functional programming languages Part III: program transformations
• Xavier Leroy, Functional programming languages Part IV: monadic transformations, monadic programming (code)
• Cornell CS, Functional Programming in OCaml: Monads

Advanced Operational Semantics

• Big-step operational semantics review
• Environment/closure-based operational semantics
• Church's lambda-calculus, reduction, and small-step operational semantics

Resources:

• Xavier Leroy, Functional programming languages Part I: interpreters and operational semantics
• Peter Selinger, Lecture Notes on the Lambda Calculus

Program Analysis

We will cover this topic in depth, implementing both abstract interpreters and symbolic evaluators for higher-order languages.

• Abstract interpretation
• Symbolic Execution

• Van Horn and Might, Abstracting Abstract Machines
• Aldrich and Le Goues, Lecture Notes: Satisfiability Modulo Theories

Advanced typed systems

We are going to cover basic type theory in detail (forall, exists, kinds) and spend less time on the advanced topics since they constitute a whole course if done rigorously.

• Forall, exists
• Higher kinds and type functions
• Recursive types
• Effect types
• Ownership types
• Gradual types
• Dependent types

• MPI-SWS, Semantics of Type Systems Lecture Notes: covers the basics, system F, recursive types.

Program verification

• Program logics
• Satisfiability Modulo Theories
• Inductive definitions
• The Coq Theorem prover

• Aldrich and Le Goues, Lecture Notes: Axiomatic Semantics and Hoare-style Verification
• Arnd Poetzsch-Heffter et al., Inductive Definitions and Fixed Points
• Cornell CS, Coq Tutorial

Assignments Outline

Here is an outline for the assignments. See the dateline for the assignments we settle on, and the due dates.

1. Transforming Fb programs in OCaml: closure conversion, A-Translation, defunctionalization, CPS.
2. An environment-based Fb interpreter in OCaml
3. Monadic programming in OCaml
4. An Fb environment/closure-based interpreter in OCaml
5. An Fb abstract interpreter in OCaml
6. An Fb symbolic evaluator in OCaml using the Z3 SMT solver
7. Correctness proofs in Coq

Potential Tutorial topics for paper reading Fridays

• Aldrich and Le Goues, Model Checking and Linear Temporal Logic
• First-order program analysis. Via e.g. Aldrich course.
• Some of the advanced types topics such as ownership types and gradual types.
• A Survey of Symbolic Execution Techniques - the broader view of symbolic execution.