Advanced Topics in Programming Languages (R04)
Organisation
This is a reading group covering a range of topics in Programming
Languages. That's a very broad subject, including language design,
semantics, compilers, analysis, verification, etc., so we can only
touch on a selection of the important ideas.
Each week we'll focus on one or two papers, as in the schedule
below. Everyone should read all of these before the meeting. One
person will be assigned (by me) to present each paper, or one person
for each part of the longer ones. That person should prepare a
presentation:
- usually 15-20 minutes long (practice beforehand to make sure it
fits)
- You should explain the problem being addressed, the approach and
the key ideas and examples, the context of related work (before and after), and
an assessment of the extent to which it solves that problem.
It often won't be possible to cover all the content of the
paper. Don't just go through the paper step by step - remember that
everyone will
have read it.
- You should prepare slides (I strongly suggest using LaTeX,
perhaps with the "prosper" or "beamer" package). A printout of these must be
handed in, with a coversheet, at the meeting.
- It's likely that you'll need to do some further reading, as part
of this preparation, to understand the paper - of some of the
citations or some background from textbooks. There are some useful
links below.
Everyone else, of course, should be prepared to discuss the work, and
to ask (or answer!) questions.
In addition to this, in the Lent term you'll be asked to produce a
written literature review, addressing some topic suggested by you and
agreed with me before the midpoint of term. This should be
between 10-15 pages (in A4, 11pt, 1 inch margins, including references).
The deadline will be at the end of term.
Assessment will be based on (a) attendence and participation in class,
(b) presentations, and (c) your literature review.
Michaelmas 2009 (Mondays 3-4pm, SW01)
Preamble
Some Classics
- Week 2 (Mon 19 Oct). Using inductively defined relations.
- A Structural Approach to Operational Semantics (Sections 1-3). Gordon
Plotkin. Technical Report DAIMI FN-19, Computer Science Department,
Aarhus University, Aarhus, Denmark, September 1981.
(later in J. Log. Algebr. Program. 60-61: 17-139 (2004)).
pdf
- (Sections 5-7)
- Week 3 (Mon 26 Oct). Concepts.
- The next 700 programming languages. Peter J. Landin. Communications of the ACM, 9(3):157-166, March 1966. pdf
- Fundamental concepts in programming languages. Christopher Strachey. Lecture Notes, International Summer School in Computer Programming, Copenhagen, August 1967. Reprinted in Higher-Order and Symbolic Computation, 13(1/2), pp. 1-49, 2000.
pdf
- Week 4 (Mon 2 Nov). Axiomatic, Observational, Denotational
- An Axiomatic Basis for Computer Programming. C. A. R. Hoare. Communications of the ACM, 12(10):576-580 and 583, October 1969. pdf
-
LCF considered as a programming language. Gordon D. Plotkin. Theoretical Computer Science, 5:223-255, 1977.
pdf
- Week 5 (Mon 9 Nov). Type quantifiers.
-
A theory of type polymorphism in programming. Robin Milner. Journal of Computer and System Sciences, 17:348-375, August 1978.
pdf
- Abstract types have existential type. John C. Mitchell,
Gordon D. Plotkin. ACM Transactions on
Programming Languages and Systems (TOPLAS), 10(3), 470 - 502, July 1988.
pdf
Low-level Semantics and Compilation
- Week 6 (Mon 16 Nov)
- From System-F to typed assembly language. (Sections 1-3:
overview and source language) Greg Morrisett, David Walker, Karl Crary, and Neal Glew. ACM Transactions on Programming Languages and Systems, 21(3):527-568, May 1999.
pdf. This is subdivided into four
parts over two weeks - the presentation for each part will need to
include some background.
- (Section 4: CPS)
- Week 7 (Mon 23 Nov)
- (Section 5: Closure conversion)
- (Section 6-8: The rest)
- Week 8 (Mon 30 Nov)
Michaelmas Paper Assignment (version 4, of 14 Oct)
Alex Katovsky | Week 2a (SOS) |
Matko Botincan (PhD) | Week 2b (SOS) |
Samuel Olatanji | Week 3a (Next 700) |
Kwok Ho Cheung | Week 3b (Concepts) |
Steffen Loesch | Week 4a (Axiomatic) |
Maciej Wos | Week 4b (LCF) |
Danish Zeb | Week 5a (Type Poly) |
Alex Katovsky | Week 5b (Abstract) |
Steffen Loesch | Week 6a (F-to-TAL, 1-3) |
Samuel Olatanji | Week 6b (F-to-TAL, CPS) |
Kwok Ho Cheung | Week 7a (F-to-TAL, Closure conversion) |
Maciej Wos | Week 7b (F-to-TAL, the rest) |
Danish Zeb | Week 8a (CompCert) |
Matko Botincan (PhD) | Week 8b (BZ) |
Lent 2010 (Thursdays 2-4pm, SW01, 28 Jan, 4 Feb, 25 Feb, 4 Mar)
(Outline Schedule!)
Students
- Matko Botincan (PhD)
- Kwok Ho Cheung
- Alexander Katovsky
- Steffen Loesch
- Samuel Olatanji
- Maciej Wos
- Danish Zeb
Links
Searching
Books
Conferences and Journals
Many of the main conferences (e.g. POPL, PLDI, ICFP, ESOP, OOPSLA,
ECOOP) are linked to from
the ACM SIGPLAN
or
ETAPS pages.
A couple of the main journals:
TOPLAS,
JFP.
Undergraduate lecture courses
Misc