*Note that the information below applies to the
CIS500 ***course**. The syllabus for the
Software Foundations area of the WPE-I can be found here.
This course introduces basic concepts and techniques in the
foundational study of programming languages, as well as their
formal logical underpinnings. The central theme is the view of
individual programs and whole languages as mathematical objects
about which precise claims may be made and proved. Particular
topics include operational techniques for formal definition of
language features, type systems and type safety properties,
polymorphism and subtyping, and foundations of object-oriented
programming.

### Grading:

Breakdown for the course grade is as follows:

- Homework: 20%
- Midterm 1: 20%
- Midterm 2: 20%
- Final Exam: 40%

#### Homework

Homework can be submitted via Blackboard.
If you are taking the course but cannot access the CIS 500
Blackboard, please contact one of the TAs.

When submitting Coq files as homeworks, please make
sure that Coq accepts your file in its entirety. If it
does not, **it will not be graded**. You can
use `Admitted` to force Coq to accept incomplete
proofs.

Homework is due before class. Late homework
submissions will be accepted for up to three days, with a
25% reduction in credit per late day (25% for one
day, 50% for two, and 75% for three).

### Prerequisites:

An undergraduate-level course in programming languages or
compilers; significant programming experience.

### Syllabus:

- Part I: Foundations
- Functional programming
- Constructive logic
- Inductive definitions and proof techniques for informal and formal proof
- The Coq proof assistant
- Part II: Basics
- Operational semantics
- Semantics of the imperative While language
- Part III: Type systems
- Simply typed λ-calculus
- Type safety
- Subtyping
- Dependently typed programming

### Textbook:

Types and Programming Languages.
Benjamin C. Pierce.
MIT Press, 2002.

### Note:

CIS500 this year is slightly different from last year, and
very different from the year before.