###
433-670

Principles of Programming Languages

Semester 1, 2002

## Staff

Lecturer: Martin Sulzmann (sulzmann@cs.mu.oz.au), L2.09
## Lectures

Wednesday 9-11am (B1.24)
** Please note the change **

## Misc

Here's a rough overview
of the course.
Downloading hugs .

Reading material on Haskell:

Haskell: The Craft of Functional Programming by Simon Thompson, Addison-Wesley, second edition, 1999,
ISBN 0-201-34275-8. The text is also on reserve in the Engineering Library.
Reading matieral on Semantics (not required, the additional material covered
won't be examinable):

The Formal Semantics of Programming Languages by Glynn Winskel
(available in the library).
433-141 Subject Notes and Exercises and Student Manual Volume A, both of which are
available from the University Bookroom.
FAQ
## Printing pdf files

1) using acroread open the pdf file
2) print - print to file temp.ps
3) mpage -2 temp.ps > temp-2p.ps
4) using ghostview or gs to check temp-2p.ps
5) lpr -Pss1 temp-2p.ps
## Midterm

Here are the results
and a sample solution.
## Errata

The lambda expression for the natural number 2 should read:
2 = lambda.f.lambda.S.f (f s) instead of
2 = lambda.f.lambda.x.f (f s).
## Final exam

Mon 17 June, 2.15pm, 2 hours, 15 min reading time
closed book exam
no calculators permitted
no additional material will be provided
Content: everything except effect systems

### Class Week Twelve (May 27-31)

Topic: Effect systems, review

Lecture material see Week 11, updated! [Wed May 29 10:57:28 EST 2002]
Midterm review, 11am-12.00, L2.09 (my office)
### Class Week Eleven (May 20-24)

Topic: More on System F, dependent types

Lecture notes in ps
and pdf format
(Contains material which will be discussed in Week 12).
Here are some comments and fixes
to some typos.
### Class Week Ten (May 13-17)

Topic: More on type systems

How to evaluate let-statements
can be found here
A note
on substitution.
Lecture notes in ps
and pdf format.
### Class Week Nine (May 6-10)

Topic: Type inference for the simply-typed lambda calculus,
second-order extensions

Updated lecture notes from Week Seven.
Algorithm W example .
New substitution notation [Updated Tue May 14 11:53:04 EST 2002].
Missing cases
for W.
### Class Week Eight (April 29 - May 3)

No lectures this week due to illness.
### Class Week Seven (April 22-26)

Topic: Simply-typed lambda calculus

Lecture notes in ps
and pdf format.
(fixed a typo on page 11, and another typo on page 12,
added unification procedure
Sat May 4 12:27:18 EST 2002)
### Class Week Six (April 15-19)

Topic: Midterm, Type systems

Midterm: 5 minutes reading time, 30 minutes exam time,
counts for 30% of the overall grade.
Please come early. Topic: everything including Lambda Calculus.
Intro to Type systems in ps
and pdf format.
### Class Week Five (April 8-12)

Topic: The lambda calculus

some comments
on exceptions.
Lectures notes in ps
and pdf format
plus some comments .
(fixed some typos 15.04)
### Easter break (April 1-5)

### Class Week Four (March 25-29)

Topic: Adding exceptions to IMP, discussion of previous excercises

Log of lecture plus questions,
week4 .
Incorporating exceptions into IMP,
ImpException.hs .
There's a connection between exceptions and algebraic data types,
see
ExceptionsVsAlgebraic.hs .
Some excercies/solutions on proof trees,
imp-ex1.txt ,
imp-ex2.txt
### Class Week Three (March 18-22)

Topic: IMP
** Please note, no lecture on Mondays from now on.
However, we'll already start at 9am on Wednesdays! **

Slides on IMP in ps
and pdf format.
(updated, more on local variable definitions, fixed a typo!)
An implementation of IMP's operational semantics can be found
here . Complete the missing cases if you like.
Log of the lecture plus questions, week3 .
I've updated the example from week 3 and incorporated the syntactic notation
for local variable declarations,
example .
### Class Week Two (March 11-15)

Topic: ABEXP

Log of Monday lecture and
some questions.
Single vs double-colons:
I sometimes write |- e :: Int where I mean to write
|- e : Int. The double-colon notation is commonly used in Haskell,
whereas we will generally use single-colons.
Arrow notation: plus : Int -> Int -> Int states that
plus is a function which takes two arguments of type Int and return
an Int. More about arrows can be found here .
Attempt to implement ABEXPs
dynamic semantics .
Adding Int v Bool to ABEXP breaks its operational semantics,
e.g. |- Int + False : Int v Bool but what would be its operational
meaning?
IMP's static semantics, tricky part local variable definitions.
See lecture nots imp.ps(pdf).
Here you can find some examples
and questions.
### Class Week One (March 4-8)

Topic: Introduction, AEXP, static and dynamic semantics

AEXP: a simple language of arithmetic expressions.
Evaluator written in Haskell: Aexp.hs
Slides in pdf and
ps format
(note I've fixed some typos)
Algebraic data types.
Algebraic.hs contains some examples
Notation introduced:
Judgments (see lec1.ps)
Proof trees
Homework
Write down the proof tree for |- ((1 / 2) * 4) + 3 :: Int
Evaluate 1 / 0

Martin SULZMANN
Last modified: Wed May 29 10:58:07 EST 2002