CSE526 (Spring `01)
Principles of Programming Languages

Course description: This course is for students interested in high-level programming languages and their formal semantics. Such study enables precise reasoning about programs, their efficient implementation and easy reuse, as will be discussed in the course. The materials to be covered include operational semantics, denotational semantics, and axiomatic semantics. We will consider imperative programming languages, functional programming languages, object-oriented programming languages, logic programming languages, and programming languages with sets and maps. We will look at topics including type systems, abstraction mechanisms, efficient implementation, and declarativeness. We will also study concurrency and parallelism.

Prerequisites: CSE307 or equivalent, or undergraduate discrete math (sets, functions and relations, predicate logic) plus programming languages in two or more paradigms (C/Pascal, ML/Scheme/Lisp, Java/C++/Smalltalk/Ada, Prolog) | Credits: 3.

Instructor: Annie Liu | Email: liuATcsDOTsunysbDOTedu | Office: Computer Science 1433, 632-8463.

TA: Jelena Trajkovic | Email: jelenaATcsDOTsunysbDOTedu | Phone: 216-2208.

Hours: Tue Thu 9:50-11:10AM, in Life Science 030 | Annie's office hours: Tue 11:10AM-12:10PM, Thu 8:50-8:50AM, 12:10:PM-1:10PM, in CS 1433 | Jelena's office hours: Mon Wed 4-5PM, in CS 2110.

Textbook: The main text is The Formal Semantics of Programming Languages by Glynn Winskel, The MIT Press, 1993. For supplemental texts and complete references, see the Readings section. In addition, you should take good notes during the lectures.

Grading: Weekly assignments, some of which require programming, together worth 50% of the grade; a midterm exam and a course project, each worth 25% of the grade. No late assignment will be accepted. Homework must be done independently; you may discuss with others and look up references, but you must write up your solutions independently. Any plagiarism or other forms of cheating will result in an F.

Course homepage: http://www.cs.sunysb.edu/~liu/cse526/, containing all course related information.

We will start with the study of formal semantics for a simple imperative language, based on the main textbook by Winskel. This introduces operational semantics, denotational semantics, and axiomatic semantics and exploits techniques for proof by induction.

We will then look at functional languages, using ML as a main example, and study their formal semantics, covering the basics and overviewing more advanced topics. We will introduce also type systems and abstraction mechanisms, based on supplemental notes.

We will then look at object-oriented languages, discussing the main concepts, emphasizing their usage for abstraction, modeling, and code reuse. This will be followed by a review and a midterm exam.

We then look at programming with sets and maps, showing up more in high-level languages, regardless of the paradigms, as abstract data types, classes, modules, packages, as well as built-in primitives. We mainly study efficient implementations, based on a novel work.

Afterward, we will look at logic programming languages, mainly Prolog, study their semantics, and discuss declarativeness, applications, and efficient implementation.

Finally, we will study nondeterminism and concurrency, based on the last chapter of the main textbook, introducing guarded commands, CSP, and CCS, as well as a specification language and model checking.

Lecture 1 (01/25/01): Overview. Program languages: general purpose, executable, high-level; principles: facilitate reasoning, productive programming, correctness proof, efficient implementation; concepts, paradigms, trade-offs; formal semantics. Reading: Chapter 1 of Winskel. Homework: Handout H1.

Lecture 2 (01/31/01): Introduction to operational semantics. A simple imperative language; evaluation of arithmetic and boolean expressions, execution of commands; equivalence relations; big-step vs small-step semantics. Reading: Chapter 2 of Winskel. Homework: Handout H2.

Lecture 3 (02/01/01) Induction and proving properties about programs and semantics. Mathematical induction, course-of-value induction; well-founded induction; structural induction, induction on derivations. Reading: Chapter 3 of Winskel. Homework: Handout H2.

Lecture 4 (02/06/01) Inductively defined sets. R-closed sets and least R-closed sets. Rule induction and special rule induction; operators and least fixed points. Reading: Chapter 4 of Winskel. Homework: Handout H3.

Lecture 5 (02/08/01) Introduction to denotational semantics. Review of OS and proving properties by induction; meaning functions, denotations of expressions and commands, least fixed point for while, equivalence of OS and DS. Reading: Sections 5.1-5.3. Homework: Handout H3.

Lecture 6 (02/13/01) Least fixed points. Meaning of while, as least fixed points of operators for adding sets of pairs; from operations on sets to continuous functions on complete partial orders; fixed-point theorem. Reading: Sections 5.4-5.6. Homework: Handout H4.

Lecture 7 (02/15/01) Introduction to axiomatic semantics. Review of DS and least fixed point; partial correctness assertions vs total correctness assertions; assertion language, substitution, interpretation. Reading: Sections 6.1-6.3. Homework: Handout H4.

Lecture 8 (02/20/01) Proof rules for partial correctness; an example proof; program development; weakest precondition; predicate transformer; soundness and completeness results. Reading: Sections 6.4-6.7, Chapter 7, proofs not required. Homework: Handout H5.

Lecture 9 (02/22/01) Functional languages and ML. Review; basics of functional languages, ML; local scoping; higher-order functions, partial application, lambda, currying; data types; pattern matching. Reading: Core Language Chapter of Harper. Homework: Handout H5.

Lecture 10 (02/27/01) More on functional languages and ML. Review; polymorphism, type inference; abstracting control structures; ML modules: structure, signature, functor (to finish). Reading: Core Language Chapter of Harper, Lecture 1 of Tofte, Handout lecture notes. Homework: Handout H6.

Lecture 11 (03/01/01) Recursion equations and parameter passing. Review, ML modules; simple recursive functions, CBV and CBN, OS and DS and equivalence, let and letrec, function scope. Reading: Chapters 8-9, details of 8.3,8.4,9.3,9.6,and proofs not required. Homework: Handout H6.

Lecture 12 (03/08/01) Higher-order functions. Review, eager vs lazy; higher-order types, product types; OS for CBV and CBN, static vs dynamic scope; overview of DS, soundness, adequacy, full abstraction, lambda calculus, PCF. Reading: Chapter 11, details of 11.3 and 11.7, 11.9, and proofs not required. Homework: Handout H7.

Lecture 13 (03/13/01) Simple type inference. Review, lambda calculus; Curry-Hindley type system; type inference: principal type scheme, constraints, unification (to finish). Reading: Lecture notes sections 1-4 of Michael Schwartzbach. Homework: Handout H7.

Lecture 14 (03/15/01) Curry-Howard isomorphism and polymorphic type inference. Review; Curry-Howard isomorphism, prod,sum,rec types; polymorphism, polymorphic type inference, polymorphic recursion. Reading: Lecture notes sections 5-9 of Michael Schwartzbach. Homework: Handout H8.

Spring break: March 19-23.

Lecture 15 (03/27/01) Object-oriented languages and Java. Encapsulation, modeling interaction, reuse; objects, classes, inheritance, method lookup; object types and subtyping. Reading: OO Concepts of Java Tutorial, Handout lecture notes. Homework: Handout H9.

Lecture 16 (03/29/01) Object-oriented programming. Design of classes and methods: implementing evaluators, FUN and OO styles; design patterns: visitor, command, flyweight, change and reuse driven. Reading: Handout lecture notes. Homework: Handout H9.

Lecture 17 (04/03/01) Midterm review. Going through all sample problems, and answering all questions. Reading: Handout preparation sheet. Homework: Solve all sample problems well; if you have any questions, come and ask; I will be in all day tomorrow.

Midterm (04/05/01) In class exam. Open textbook, other assigned readings, handout lecture notes, and your own handwritten (not mechanically or electronically reproduced) notes. Closed all other items. Homework: Relax, as the rest will be easier and more fun.

Lecture 18 (04/10/01) Programming with sets and maps. Clarity and inefficiency; SETL, set and map operations, general set formers, other set-related expressions and statements, Java2 APIs; topological sort, reachability, strongly connected components. Reading: Handout lecture notes, SETL2 Programming Language. Homework: Handout H10.

Lecture 19 (04/12/01) From clear description to efficient implementation. High-level and low-level SETL, reachability example, SQ+ to C; dominated convergence, finite differencing, real-time simulation. Reading: Handout lecture notes. Homework: Handout H10.

Lecture 20 (04/17/01) Finite differencing of set expressions. Basic ideas; derivative, w.r.t. code block; sequential composition, chain rule; expensive exps, auxiliary maps; putting all together; reachability, SCC. Reading: Handout lecture notes, paper by Paige and Koenig not required. Homework: Handout H11.

lecture 21 (04/19/01) Real-time simulation of set operations on a RAM; classes of operations; based representations; type constraints, determined by operations, determining representations. Reading: Handout lecture notes. Homework: Handout H11.

lecture 22 (04/24/01) Logic programming and Prolog. Logic programs, syntax, Prolog; logic programming, relational database programming, recursive functional programming, but more. Reading: Handout lecture notes, Tutorial Sections 1-3 of Apt. Homework: Handout H12.

lecture 23 (04/26/01) Logic programs semantics, implementation, and efficiency. Operational: unification, SLD resolution; declarative: Herbrand model; denotational semantics; implementation and efficiency: negation, cut, tables, reachability. Reading: Handout lecture notes, Tutorial Section 5.2 of XSB Manual Vol 1. Homework: Handout H12.

lecture 24 (05/01/01) Project description, nondeterminism and concurrency. Project description; guarded commands, communicating processes, CSP, CCS, operational semantics, examples. Reading: Handout lecture notes, Sections 14.1-14.4 of Winskel. Homework: Project, see Handout P.

lecture 25 (05/03/01) Project questions and answers, specifying and checking properties of processes. Modal mu-calculus, modality, fixed points; model checking, global and local/on-the-fly; examples. Reading: Sections 14.6-14.8. Homework: Project, see Handout P.

lecture 26 (05/08/01) Summary and presentations. Comparing programs for reachability written in different languages and at different levels. Homework: Project, see Handout P.

Handout Q: Questionnaire

Handout H1: Homework 1: Basic Set Theory

Handout H2: Homework 2: Implementing an Operational Semantics

Handout H3: Homework 3: Rules and Proving Properties about Programs and Semantics

Handout H4: Homework 4: Denotational Semantics and Least Fixed Points

Handout H5: Homework 5: Axiomatic Semantics and Proofs of Partial Correctness Assertions

Handout H6: Homework 6: Functional Programming in ML

Handout H7: Homework 7: Translating and Interpreting Recursive Functions, in ML | Outline and comments

Handout H8: Homework 8: Higher-Order Functions and Polymorphic Type Inference

Handout H9: Homework 9: Interpreter for an Imperative Language with Aliasing and I/O, in Java

Handout H10: Homework 10: Programming with High-Level Set and Map Operations in Java

Handout H11: Homework 11: Implementing Graph Reachability using Set and Map Operations in Java

Handout H12: Homework 12: Generating C from SQ+ and Programming in Prolog

Handout L10: Notes for Lecture 10: Functional languages and ML

Handout L15: Notes for Lecture 15: Object-oriented languages and Java

Handout L16: Notes for Lecture 16: Object-oriented programming

Handout L18: Notes for Lecture 18: Programming with sets and maps

Handout L19: Notes for Lecture 19: From clear description to efficient implementation

Handout L20: Notes for Lecture 20: Finite differencing of set expressions

Handout L21: Notes for Lecture 21: Real-time simulation of set operations

Handout L22: Notes for Lecture 22: Logic programming and Prolog

Handout L23: Notes for Lecture 23: Logic programs semantics, implementation, and efficiency

Handout L24: Notes for Lecture 24: Nondeterminism and concurrency; Project description

Handout E1: Preparation for Midterm Exam

Handout E2: Midterm Exam

Handout E3: Solution to Midterm Exam

Handout P: Project Description | Project Summary

Basic set theory: Chapter 1 of Winskel

Formal semantics for a simple imperative language: Chapters 2-7 of Winskel

Functional languages and SML:
Programming in Standard ML by Bob Harper (for others, see SML/NJ Literature)
Four Lectures on Standard ML by Mads Tofte (1-3)
Chapters 8, 9, and 11 of Winskel
Lecture Notes on Polymorphic Type Inference by Michael I. Schwartzbach

Object-oriented languages and Java:
Lesson on OO Programming Concepts in The Java Tutorial
Handout Lecture Notes L15 and L16
API Specification of Java2 (for reference only)
The Collections Framework in Java2

Programming with sets and maps:
The SETL2 Programming Language by W. Kirk Snyder (parts 2 and 3)
Handout Lecture Notes L18 and L19
Handout Lecture Notes L20 and L21

Logic programming language and Prolog:
The Logic Programming Paradigm: A Tutorial by Krzysztof R. Apt (sections 1-3)
Handout Lecture Notes L22 and L23
The XSB Programmers' Manual by Sagonas et al (section 5.2 of Vol 1)

Nondeterminism and concurrency: Chapter 14 of Winskel
Handout Lecture Notes L24

SML/NJ: Standard ML of New Jersey (local installation at /usr/shareware/bin/njsml.dir/)

Java2: version 1.2 | version 1.3

SETL2: A set-based programming language (guide to installation)

XSB: A logic programming and deductive database system (local installation at /usr/shareware/bin/xsb.dir/)

Old APTS (guide to local installation, usage, examples)