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