Schedule and Topics
My Office Hour
Tuesday 10:00 – 11:00, Building E1.1, Room U18
Here are some details about the Language-based Security tutorial (the authoritative source of information remains the website of the lecture). The tutorial takes place every Wednesday from 9:15 to 10:45 (the lecture is given immediately afterwards – 11:15 to 12:45), and every second week we have a 20 minutes quiz. The quizzes count for 30% of the final grade, and the worst graded quiz is not considered for the final grade. An average of 50% in the quizzes is required to be accepted in the final exam.
One more thing which is not very common around here is that tutorials start on the first week. Immediately after the first lecture, we will do very basic things related to the lambda calculus and operational semantics. Things like the inductive definitions of terms and derivations, recursively defined functions, structural recursion on terms and derivations. We will also gain more intuition and try out examples about the basics of lambda calculus (concrete vs abstract syntax, capture-avoiding substitutions, values, stuckness, divergence). Sure, many won’t need this kind of introduction, but remember that tutorials are optional (unless there is a quiz). And I think it will be very useful for those who have never seen a lambda in their whole life.
Additional Reading (To be extended)
These are just papers I enjoyed reading while preparing for this tutorial. They are not reading material required for this lecture.
- Philip Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing. 2000
- Luca Cardelli. Type Systems. 1997
- Lantian Zheng, Andrew C. Myers. Dynamic Security Labels and Noninterference. 2004.
- François Pottier and Vincent Simonet. Information Flow Inference for ML. 2003
- Andrei Sabelfeld and David Sands. A Per Model of Secure Information Flow in Sequential Programs. 2001.
Typed Assembly Language
- Gred Morrisett and David Walker. From System F to Typed Assembly Language. 1999
- Greg Morrisett, et. all. Stack-Based Typed Assembly Language. 2002.
- Nick Benton. A Typed, Compositional Logic for a Stack-Based Abstract Machine. 2005.
- Benjamin Pierce. Chapter 5 of Advanced Topics in Types and Programming Languages. 2005.
- George C. Necula, et all. A Certifying Compiler for Java. 2000
- Aleph One. Smashing The Stack For Fun And Profit.
- Gred Morrisett, et all. Cyclone: A Type-Safe Dialect of C. 2004