CMSC 32001

Topics in Programming Languages

Prerequisites: Consent of instructor.

For Autumn 2009, the prerequisites are:

Programming experience, particularly in some functional language such as Scheme, ML, or Haskell would be useful. Some familiarity with basic concepts of set theory and logic, as covered in CMSC 15300 (Foundations of Software) for instance, is required. An undergraduate programming language course such as CMSC 22100 (Programming Languages) would provide useful background.

Catalog Description: This course covers a selection of advanced topics in programming languages.

For Autumn 2009, the topic will be Interactive Proof and Mechanized Metatheory in Coq.

Long Description: The description can vary depending on the particular topic.

Here is the description for the Autumn 2009 Topics in Programming Languages course:

This course introduces the techniques of interactive theorem proving using the Coq system. Coq uses a type-theoretic logic that is similar to a typed functional programming language, and it has become important in recent years as a tool in the foundational study of programming languages ("mechanized metatheory"), in the verification of programs and system designs, and in producing mechanically verified proofs of difficult mathematical theorems such as the Four Color problem.

Applications for Coq theorem proving will be taken primarily from the foundational study of programming languages. The central theme is that individual programs and whole languages are viewed as mathematical objects that can be formalized in Coq and about which precise claims may be made an proved.

Particular topics may include operational techniques for formal definition of language features, type systems and type safety properties, polymorphism and subtyping.

The primary text is "Interactive Theorem Proving and Program Development" by Yves Bertot and Pierre CastEran [Springer, 2004]. The course will use the first nine chapters. A supplementary text is "Types and Programming Languages" by Benjamin C. Pierce, which provides background material on the operational semantics of programming languages, type systems, etc.

Instructors: Dave MacQueen (for Autumn 2009)
Quarter offered:
Unverified as of 23 November, 2009.