CS 6202
Course details
- Semester 1 2006/7
- Lectures: Tuesday 14.00 pm - 16.00 pm;
Venue: Room 405, 4th Floor, S16.
- Lecturer: Chin Wei-Ngan.
Announcement
- Week 0: Introductory
Lecture at 2:00pm, 8th August 2006.
-
Makeup
Lecture at 4-6pm, 31st August 2006, MR3, Level 5, SoC1
-
Lecture on 19th Sept
(Tue) cancelled.
-
Next lectures on 3,10 Oct
will be on Separation Logic.
-
We will schedule survey
paper presentations on 17th Oct.
Course description
This module focuses on advanced features and foundations of programming
languages. The aim of the course is to look at latest language issues and
tools that can facilitate software programming project. While the course will
cover some state-of-the-art research topics on language features and reasoning
systems, we envision that familiarity with these language/tools to be helpful
for students pursuing programming projects for a diverse range of topics.
The first part of the course will comprise of a series of lectures on advance
language features in Standard ML and Java 5, and foundations of type system and
logic to support the reasoning of programs written in declarative and imperative
programming.
In the second-half of the
course, students will undertake in depth reading and
exploration into selected topics of current research
areas on programming languages and their applications. Students
will have opportunity to present their findings,
culminating in a term paper report.
Grading
- Assignments (30%).
- Test/Quizes (20%).
- Term paper - project (50%).
Course outline
- Standard ML - An Advanced Language.
- Type System for Lightweight Analysis.
- Genericity for OO (Wildcard Types in Java 5).
- Formal Reasoning - Separation Logic and Theorem Proving.
- Term Paper MiniProjects.
Lecture notes
- Lecture 0 - Introduction (pdf, pdf 4-in-1), Why Generic Java? (pdf, pdf 4-in-1).
- Lecture 1 - Lambda Calculus (pdf, pdf 4-in-1).
- Lecture 2 + Lecture 3 - ML (pdf, pdf 4-in-1).
- Lecture 4 + Lecture 5 - Types for Extended Lambda Calculus (pdf, pdf 4-in-1).
- Lecture 6 - Type Reconstruction (pdf, pdf 4-in-1).
- Lecture 7 - Universal/Existential Types (pdf, pdf 4-in-1).
- Lecture 8 + Lecture 9 - Separation Logic (pdf, pdf 4-in-1).
- Lecture 10 - Java Generics and Collections (pdf, pdf 4-in-1).
- Lecture 11 - Java Generics and Collections (pdf, pdf 4-in-1).
Assignments
- Assignment 1 (pdf) - DEADLINE 1 September, 8PM.
- Assignment 2 (pdf) (Updated with examples) - Code - DEADLINE 25 September, 8PM.
Online Resources
- John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, (invited paper, LICS'02). (pdf)
- Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin, Automated Verification of Shape and Size Properties via Separation Logic, (submitted for publication).
(draft paper), (demo)
Additional Links