The course covers the mathematical and formal foundations of modern programming languages. Topics include: syntax and semantics of three paradigm languages, one functional (PCF), one object oriented and one foundational (the lambda calculus); the operational, axiomatic and denotational semantics of programming languages; program verification; topics in the typed and untyped lambda-calculus; topics in type theory (type inference, subtyping, polymorphism). Material presented in class, or assigned for independent reading, will be mostly from the textbook and occasionally from handouts.

There is no programming in this course, but you will appreciate the value of the course in proportion to your programming experience and familiarity with different programming paradigms. If you have never programmed before, the material will come across as dry and formal, with little or no practical motivation for it. And I venture to say that the better programmer you are, the easier the course will be for you.

• Homework assignments, about 40% of final grade
• Midterm exam (one hour), about 25%
• End-of-term exam (two hours), about 35%

• Midterm: 10.24.01 10-11 am
• Final: 12.19.01 9-11 am

• Problems will be assigned every week. All problems assigned one week are due the following week. Homework problems returned after their due date will not be graded.
 
• Collaboration in homework assignments is accepted, but not encouraged (In an undergraduate course, this is an absolute no-no). Always try to do the homework problems on your own first. If you get stuck and decide to collaborate with someone else in the class on a homework problem, you have to acknowledge it: Mention the name of your partner at the beginning of any joint solution you hand in. Just be aware that there is an official BU document called the "Academic Conduct Code".
 
• The expected work is 3 hours of lecture per week + 9 hours of studying on your own per week (reviewing lecture notes, homework problems, additional material) -- for a total of 12 hours per week.

• The tests are closed book. You may, however, bring one 8.5 by 11 sheet of paper (i.e. one regular-size sheet of paper) as a crib sheet. Preparing a crib sheet can be a useful study aid, so take time in selecting material for it. You may use both sides of the paper and write as small as you like, but in any case, you are allowed only one sheet. No mechanical or electronic reproductions are allowed; the crib sheet must be hand written. You must hand in your crib sheet when you hand in your test, and you will get credit for it in your total grade for the test.
 
• For each test, you are responsible for material covered in lecture, in problem sets, and in the corresponding sections in the textbook -- up to the date of that test. Although the end-of-term test will cover the entire course, it will emphasize the latter part of the course (after the mid-term test).
 
• You cannot miss a test! In case of an emergency forcing you to miss a test, please bring the matter to my attention.

• To join the course mailing list, type csmail -a cs520 at the Unix prompt
• To inspect who else is on the mailing list, type csmail -p cs520
• To remove yourself from the mailing list, type csmail -r cs520

• "Foundations for Programming Languages", John C. Mitchell, The MIT Press, 1996. [Errata]
 
• "A Theory of Objects", Martin Abadi and Luca Cardelli, Springer, 1996.

• Sigma : An interpreter for the Sigma Calculus with lambdas. 

• Problem Set 1 (due 9.19.2001) [Solutions]
• Problem Set 2 (due 9.26.2001) [Solutions]
• Problem Set 3 (due 10.5.2001) [Solutions]
• Problem Set 4 (due 10.15.2001) [Solutions]
• Problem Set 5 (due 10.22.2001) [Solutions]
• Problem Set 6 (due 11.5.2001)
• Problem Set 7 (due 11.14.2001) [Solutions]
• Problem Set 8 (due 11.26.2001) [Solutions]
• Problem Set 9 (due 12.10.2001) [Solutions]

• Week 1: Lambda notation. Introduction to semantics. Syntax vs. Semantics. Induction.
   
• Week 2: More on Induction. Introduction to the Language PCF.
   
• Week 3: The Language PCF: syntax and operational semantics.
   
• Week 4: The Language PCF: type system, axiomatic semantics, denotational semantics, extensions.
   
• Week 5: Simply-typed Lambda Calculus: context-sensitive syntax, product and sum types and related types.
   
• Week 6: Simply-typed Lambda Calculus: Curry-Howard isomorphism, type checking.
   
• Week 7: Simply-typed Lambda Calculus: Henkin models. Midterm.
   
• Week 8: Object Orientation: class-based languages, object-based languages. [Slides Ch.2] [Slides Ch.3]
   
• Week 9: Object-based languages and the Sigma Calculus. [Slides Ch.4] [Slides Ch.6]
   
• Week 10: Type systems for the Sigma Calculus. [Slides Ch.7/8]
   
• Week 11: Type Inference: Unification, Principal Types, The PT Algorithm.
   
• Week 12: Recursive Types: Extending Unification, Finite Representations, Typing Power.