Description
This course will examine the design and implementation of programming languages from a foundational perspective. Our goal will be to develop tools that will enable us to both design and specify new language features, to precisely understand the rationale for existing features in modern languages, and to understand how design decisions can impact implementations. The course will be divided into roughly three parts:
1. principles (e.g., semantics, type systems, specifications)
2. proof techniques and formal reasoning
3. automated theorem proving using the Coq proof assistant
Our discussion of principles will be crafted in the context of definitions and theorems that capture salient properties of modern languages. The validation of these theorems will be undertaken using Coq, a powerful theorem prover and mechanized proof assistant.
1. principles (e.g., semantics, type systems, specifications)
2. proof techniques and formal reasoning
3. automated theorem proving using the Coq proof assistant
Our discussion of principles will be crafted in the context of definitions and theorems that capture salient properties of modern languages. The validation of these theorems will be undertaken using Coq, a powerful theorem prover and mechanized proof assistant.
General Information
Course Website:
| Name | Office Hours | |
|---|---|---|
Benjamin Delaware | When? Where? | |
Qianchuan Ye | When? Where? |