Principles of Programming Languages

[General Information]
[Course Outline]
[Requirements]

[Announcements]
[Lectures]
[Handouts]
[Readings]
[Systems]

**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.

Homeworks and projects must be done individually; you may discuss with others and look up references, but you must write up your solutions independently and credit all sources that you used. Any plagiarism or other forms of cheating will result in an F or worse.**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.

Annie Liu