Programming languages are a fundamental part of computer science. This course introduces the formal tools needed to describe precisely what a program means. These tools help us answer many useful questions about program analyses and transformations, such as:
- Is this program correct?
- Will this program encounter a run-time type error?
- Is one program indistinguishable from another?
- Is this optimization a safe program transformation?
- Does this program compute the intended result? Does it leak information?
- Is this compiler translation correct?
- Can source language A be translated into target language B?
- Different styles of dynamic semantics, including operational, axiomatic, and denotational semantics
- Static semantics, especially type systems
- Proofs by induction on derivations and structure
- A formal treatment of important programming language features such as functions, laziness, exceptions, continuations, modules, type polymorphism, objects and classes
Instructor: Andrew Myers
|Andrew Myers||Instructor||[point here]||255-8597||Upson 4133, Monday 11-12, Thursday 11-12|
|Shrutarshi Basu||PhD TA||[point here]||[TBA]||Upson 360, 1:30–3PM|
Recommended TextsThe following books are recommended but not required:
- Types and Programming Languages, by Benjamin Pierce
- The Formal Semantics of Programming Languages, by Glynn Winskel
These books are excellent sources for the course, so purchasing them is not a bad idea. In a pinch, many students in the CS department will have this book, and they will also be on reserve at the Engineering library.
Some other useful texts that provide a different perspective or more depth in some areas are:
- Programming Languages: Theory and Practice, by Robert Harper (online draft)
- Foundations for Programming Languages, by John Mitchell
- Semantics for Programming Languages, by Carl Gunter
- Basic Category Theory for Computer Scientists, by Benjamin Pierce
- Objective CAML Tutorial
- Introduction to the Objective Caml Programming Language, by Jason Hickey (online version)
- F#, a language similar to OCaml. You can use the Visual Studio IDE to write and debug F# programs.
- Comparison of SML and OCaml, by Andreas Rossberg.
- ledit, a tool to provide emacs-like editing (and history) to the OCaml toplevel. (Info on how to use ledit, and other tips for using the toplevel, here.)
For information about which readings are associated with each lecture, see the course schedule.
Grading and submission policies
There will be 6 assignments, mostly written problems but some programming problems in OCaml, totaling to 40% of your score. The first assignment will be done solo; later ones will be done with a partner.
Assignment late penalties:
We are flexible about submitting assignments late. You will have 4 late days total during the semester. No penalty will be applied if you limit the total number of late days to 4 or less.
There will be preliminary exam, time and location TBA.
The final exam is during the final exam period (location and time TBD) and will be 30% of your score.
We expect you to participate in class and elsewhere. 5% of the score will be for participation (in-class, Piazza, course evals) and for in-class quizzes.
- OCaml home page
- OCaml support for emacs and vim
- LaTeX style files for typesetting 6110 notes
- TeX Math Symbols font for viewing course slide sets.
- CS 6110, Spring 2011
- CS 6110, Spring 2010
- CS 6110, Spring 2009
Other resources for programming assignments:
- Group project specification: Simulating Evolving Artificial Life (last update: 11/9) [ simulation constants ] (last update: 9/28)
- Overview document requirements for group project assignments