Many Notes and Announcements

Thanks for being a great audience!

Also, good work with the assignments!

• Nearly everyone's "Hindsight" code ran without headaches.
  • We have emailed the handful of students with some oddity.
• Everyone's code produced at least one wrong output.

On the topic of assignments, our first question:

• Will we release sample answers?
  • Our strong preference is not to. You can express your preferences as well, and we'll try to take them into account. The problem is, if we release the "model" solution to lots of people, we pretty much can't use those questions again. If we just give hints, we can keep questions and assignments for a few years.
  • If you have a question about a particular part, ask on the forum, and we will likely provide some clarification.

• Note from marking the "Proofs" assignment:
  • It is a bit long and slow to mark, and so we are planning on tweaking it.
  • In particular, there are some traps where students who took a wrong step ended up dealing with loads of cases.

What kind of material is likely to appear in the exam?

• The kinds of questions we've asked in tutorials are a pretty good guide.
  • Note that some tutorial questions are clearly exercises, others are more open ended and are there to provoke thought/discussion. We mean the exercises.
• There is a list of kinds of topics further down. The lecturers have checked that this list covers the exam contents.
• Monads will not appear in the exam.

You need to decide what to put into an A4 page of notes to take into the exam. Why are we so restrictive?

• It's not very useful to us to ask an exam question and get the exact same answer from everyone. If we give you lots of space, students tend to bring in all the notes, and quote long sections of them as sort-of answers when they don't know what else to do.

How can you format your notes on an A4 sheet?

• You can print something out or write it out by hand, up to you.

Will exam questions ask for pseudo-code?

• We will not ask for type-correct Haskell implementations, no.
• We might ask for simple example MinHS expressions.
• If we do ask for pseudo-code, we won't be picky about language details.
  • For instance, we won't require exact Haskell syntax or type-correctness.

An advanced student (Rob S) asks:

• If the students are asked to do a typing derivation, is it OK if it's a bit fudged?
  • It would be a problem if the derivation doesn't make sense or is vague.
  • It is important to be precise about the way rules are used.
  • It might be helpful to have various typing rules to hand.

Here is a quick summary of what we have covered and possible exam exercises on those topics:

• Gentzen style rule calculus, derivations, induction, derived and admissible rules.
• Syntax, e.g. parsing, ambiguity, language grammars.
• Static semantics, e.g. scope checking and type checking.
• Dynamic semantics, e.g. denotational and operational, and in particular the small-step and big-step variants and what they're for.
  • Proofs about small-step and big-step semantics.
• Lambda calculus.
  • Binding and capture-avoiding substitution and such headaches.
• Imperative languages.
  • In an imperative language with mutable variables, what should uninitialized values mean?
  • Hoare logic (the only axiomatic semantics/program logic in this course).
• MinHS, its base semantics, and more detailed abstract machines for evaluating MinHS more like a compiler/implementation.
  • Recall the C machine and E machine?
  • What is a frame object (an expression context with a hole) for?
  • What is an environment object (to do with variable assignments) for?
  • What do exceptions do? How do they interact with partial ops like 1/0 ?
• Safety vs liveness properties and trace properties.
  • What is a safety property vs a liveness property?
• Algebraic datatypes, sums, products, and the tricky recursive type.
  • Can we do the construction to/from Haskell-style datatypes?
• The Curry-Howard isomorphism.
  • This is a big deal to a lot of modern researchers.
  • Lots of things are named after Haskell Curry.
  • Logics can be used to invent types and language features and vice versa.
    • e.g. Polymorphism/forall-quantification.
  • Lots of exercises can be made up, take a simple logical puzzle, provide a term that proves it in the Curry-Howard style, etc.
• Polymorphism and type inference.
  • Parametric polymorphic functions (forall) and inference/instantiation.
    • What type does this expression have? What expression has this type?
  • Overloading-style polymorphism (classes) and the dictionary construction.
  • Subtype polymorphism (inheritance/coercion).
    • What is covariant? What is contravariant? What is a coercion?
    • What is a good coercion for types X and Y?
  • What do the forall quantifiers mean in type signatures?
  • What kinds of facts do we get "for free" from parametricity?
• Concurrency.
  • Concurrency issues, and the LCR constraint.
  • Shared-variable concurrency vs message-style concurrency.
  • Session types: proofs about message-style concurrency.
    • Senders should send to receivers that can receive.
    • Rob claims there are some slides that group all the key rules for session typing in the one place, so make sure you are familiar with that.
    • There are plenty of exercises we could give about typing and duals etc.

We will watch the forum through stuvac up to the exam, especially as exam prep and the final assignment are ongoing. Good luck with that!

Farewell!