CSE526 (Spring `05)
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 higher-level languages with sets and maps. We will look at topics including type systems, abstraction mechanisms, declarativeness, and efficient implementations. We will also study concurrency and parallelism.

Prerequisites: CSE307, CSE304, 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++/Python, Prolog) | Credits: 3.

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

TA: Jin Zhou | Email: jzhouATcsDOTsunysbDOTedu

Hours: Tue Thu 2:20-3:40AM, in Social & Behavioral Sciences s328 | Annie's office hours: Tue 9-10AM, Fri 3:30-4:30PM, and by appointment, in CS 1433, and before and after class | Jin's office hours: Mon Wed 11:00-11:30, in CS 2110, and by appointment.

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, written or programming, together worth 50% of the grade; a midterm exam and a course project, each worth 25% of the grade. No late submission will receive credit. Exceptions only when supported with official documents will be allowed.

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, using Python as a part of this, discussing the main concepts, emphasizing their usage for abstraction, modeling, and reuse. This will be followed by a review and a midterm exam.

We then discuss 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 an impressive work.

Afterward, we will look at logic languages, including Prolog, XSB, and FLORA that is also object-oriented, study their semantics, and discuss declarativeness, applications, and 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/05): Overview. Programming languages: general purpose, executable, high-level; principles: facilitate reasoning, productive programming, correctness proof, efficient implementation; concepts, paradigms, trade-offs; course plans. Reading: Chapter 1 of Winskel. Homework: Handout H1.

Lecture 2 (01/27/05): Formal semantics and preliminaries. Introducing operational, denotational, and axiomatic semantics; syntax directed; basic set theory: logical notations, sets and set construction, relations and functions. Reading: Chapter 1 of Winskel.

Lecture 3 (02/01/05): 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 4 (02/03/05): 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.

Lecture 5 (02/08/05): 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 6 (02/10/05): Introduction to denotational semantics. Review of proving properties on sets defined by rules; meaning functions; denotations of expressions and commands; least fixed point for while; equivalence of OS and DS. Reading: Sections 5.1-5.3.

Lecture 7 (02/15/05): 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 8 (02/17/05): 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.

Lecture 9 (02/22/05): 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 10 (02/24/05): 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.

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

Lecture 12 (03/03/05): Recursion equations and parameter passing. Review; 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.

Lecture 13 (03/08/05): 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 14 (03/10/05): 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.

Lecture 15 (03/15/05): 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.

Lecture 16 (03/17/05): Object-oriented languages and Python. OO: encapsulation around data, modeling interaction, reuse; Python basics: neat, rich; very high-level data types; classes, methods, instance creation, init, self, inheritance, method lookup; implementing evaluators, FUN vs OO styles. Reading: Python Tutorial.

Spring break: March 21-25. Have a good break! We will have more and real fun afterwards!

Lectures 17 (03/29/05) and 18 (03/31/05): Self study of Python Tutorial, looking up Python Reference Manual and Python Library Reference when necessary, for more on programming with objects and with very high level data types in Python. Reading: Python Tutorial. Homework: Handout H9.

Lecture 19 (04/05/05): 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/07/05): 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 21 (04/12/05): Programming with sets and maps. Clarity and inefficiency; SETL, set and map operations, general set formers, other set expressions and statements; reachability, topological sort, strongly connected components. Reading: Handout lecture notes. Homework: Handout H10.

Lecture 22 (04/14/05): From clear specifications to efficient implementations. High-level and low-level SETL, reachability example, SQ+ to C; dominated convergence, finite differencing, real-time simulation. Reading: Handout lecture notes.

Lecture 23 (04/19/05): Logic programming and Prolog. Logic programs, syntax, Prolog; logic programming, relational database programming, recursive functional programming, but more. Reading: Handout lecture notes, Sections 1-3 of Apt's tutorial. Homework: Handout H11.

Lecture 24 (04/21/05): Logic programs semantics, implementation, and efficiency (ref handout). Operational: unification, SLD resolution; declarative: Herbrand model; denotational semantics; implementation and efficiency: negation, cut, tabling, reachability. Reading: Handout lecture notes, Sec.5.2 of XSB's tabling tutorial.

Lecture 25 (04/26/05): Programming with objects and logic. FLORA2 introduction: F-logic, HiLog, Transaction logic; F-logic: oids, attributes, isA, methods, queries, types, virtual classes, parameterized, more queries; reachability example. Reading: Handout lecture notes. Homework: Handout H12.

Lecture 26 (4/28/05): Reachability example, HiLog, Transaction logic, project description. HiLog: variables for functors and predicates and formulas, as arguments and returns; Transaction logic: updates, sequence of DB states, backtrackable; misc FLORA2 features omitted. Reading: Handout lecture notes.

Lecture 27 (05/03/05): 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.

Handout Q: Questionnaire

Handout H1: Homework 1: Basic Set Theory

Handout H2: Homework 2: Implementing an Operational Semantics, in a language of your choice

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 Python

Handout H10: Homework 10: Implementing Graph Reachability using Set and Map Operations, in Python

Handout H11: Homework 11: Logic Programming using XSB

Handout H12: Homework 12: Programming with Objects and Logic using FLORA2

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

Handout L11: Notes for Lecture 11: More on functional languages and ML

Handout L21: Notes for Lecture 21: Programming with sets and maps

Handout L22: Notes for Lecture 22: From clear description to efficient implementation

Handout L23: Notes for Lecture 23: Logic programming and Prolog

Handout L24: Notes for Lecture 24: Logic programs semantics, implementation, and efficiency

Handout L25: Notes for Lecture 25: Programming with objects and logic

Handout L26: Notes for Lecture 26: HiLog and Transaction logic

Handout L27: Notes for Lecture 27: Nondeterminism and concurrency

Handout E1: Preparation for Midterm Exam

Handout E2: Midterm Exam

Handout E3: Solution to Midterm Exam

Handout P: Project Description

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 a recent version in pdf and others, see SML/NJ Literature)
Four Lectures on Standard ML by Mads Tofte (1-3)
Handout Lecture Notes L10 and L11
Chapters 8, 9, and 11 of Winskel
Lecture Notes on Polymorphic Type Inference by Michael I. Schwartzbach

Object-oriented languages:
Python Tutorial (Classes | Data Structures ) | Reference Manual | Library Reference
Python | Python Documentation (v2.4)
The Java Tutorial (Learning the Language | Collections Framework) | API Specifications ( J2SE 1.4 | 1.5 )
Java | J2SE Documentation | Generics and enhanced for-loop in J2SE 1.5
See FLORA2 in logic programming languages below.

Programming with sets and maps:
The SETL2 Programming Language by Kirk Snyder (parts 2 and 3)
SETL2 | SETL2 Documentation | Current developments at settheory.com
Handout Lecture Notes L21 and L22
An Invitation to SETL: An Linux Journal article (12/28/2004) | A SETL Documentation in html

Logic programming languages:
The Logic Programming Paradigm: A Tutorial by Krzysztof R. Apt (sections 1-3)
Handout Lecture Notes L23 and L24
The XSB Programmers' Manual by Sagonas et al (section 5.2 of Vol 1)
FLORA2: An Object-Oriented Knowledge Base Language | Tutorial
Handout Lecture Notes L25 and L26

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

SML/NJ: local installation at /usr/shareware/bin/njsml.dir/ (execute '/usr/shareware/bin/njsml' locally)

Python: local installation under /usr/local/ (execute '/usr/local/bin/python' locally)

SETL2: local installation under /home/facfs1/liu/tools/setl2-2.3/ (guide to your own installation)

XSB: local installation at here or, for newest version, /home/facfs1/liu/tools/XSB/ (exec 'xsb' under 'bin')

FLORA2: local installation at /home/facfs1/liu/tools/flora2/ (exec 'runflora') or ask me for the tar ball

Old APTS: guide to local installation, usage, and examples

You should learn all information on the course homepage. Check the homepage periodically for Announcements.

Do all course work. The homeworks and projects are integral parts of the course as they provide concrete experiences with the basic concepts and methods covered in the class.

Disability: If you have a physical, psychological, medical or learning disability that may have an impact on your ability to carry out assigned course work, please contact the staff in the Disabled Student Services office (DSS), Room 133 Humanities, 632-6748/TDD. DSS will review your concerns and determine with you what accommodations are necessary and appropriate. All information and documentation of disability are confidential.