3 Credit Hours
3 Credit Hours
Designed to acquaint you with the fundamental ideas behind modern programming language design and analysis. Ultimately, you should come away with the ability to apply programming language techniques to your own projects.
The course has three broad topics:
The first part of this graduate-level course focuses on the semantics of a variety of programming language features (e.g., "what does a while loop really mean?"). We will study structural operational semantics as a way to formalize the intended execution and implementation of languages. Operational semantics concepts and notation are widely used in modern programming language research. We will survey axiomatic semantics, which provides a basis for verifying programs. Axiomatic semantics underly research efforts in formal verification and bug finding (e.g., SLAM, which led to Microsoft's Static Driver Verifier). We will briefly look at denotational semantics as a prelude to abstract interpretation. Abstract interpretation also underly research efforts in program analysis and bug finding (e.g., Astrée, which has been used by Airbus to analyze their flight control software).
The second part of this course provides an introduction to the study of type systems for programming languages. We will start our study with the simply-typed lambda calculus and then touch upon more advanced features such as types for imperative features, exceptions, and abstraction. Type systems abound in modern programming languages.
The last part of the course covers special topics drawn from research in areas such as applications of program semantics to program analysis and verification.
Same as ECEN 5533.
The prerequisites for this course are programming and mathematical experience with prior exposure to several different programming languages, such as C, ML, and Java, which may be satisfied by taking CSCI 3155 or equivalent. The ideal programming experience is an undergraduate compilers course (e.g., CSCI 4555). The ideal mathematical experience is familiarity with mathematical logic and the ability to construct rigorous proofs (in particular by structural induction). These prerequisites are not strict. However, your desire to be exposed to this material is very important.
Web and e-mail access required.
Any syllabus provided above may not be the most recent version. Please refer to the course syllabus provided by the instructor of this course.