Textbook:
Online textbook: Software Foundations
Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.
WPE-I Syllabus:
- Chapters 1-3, 8, 9, 11, and 15 of TAPL, excluding Section 15.6 (Coercion Semantics for Subtyping).
- Programming with dependent types.
- Semantics for imperative programs
- Working knowledge of the Coq proof assistant and its use in formalizing proofs about programming languages. (Study materials for this part of the syllabus will be made available as the semester progresses. Students who want to take the WPE exam without sitting in on the course can get these materials from the CIS500 web page. The first nine chapters of Interactive Theorem Proving and Program Development by Yves Bertot and Pierre Castéran [Springer, 2004] may be useful as a supplemental reference.)
Note:
This syllabus largely overlaps to the material that will be covered in class and homework assignments in CIS500. The WPE-I exam itself will be the same as the CIS500 final exam. A separate (non-curved) WPE-I grade of Pass or Fail will be given in addition to the normal (curved) final exam grade for CIS500.