CS 750: Programs, Proof and types

Course Information

The course, in its offering next semester, plans to cover programming language foundations in a hands-on way through theorem prover Coq. This simultane- ously covers PL concepts as well theorem proving in Coq. For more details see the link:

https://softwarefoundations.cis.upenn.edu/.

The course intends to cover most of volume 1 and volume 2 listed on this link. If there is interest and time, we may also cover some other topics.

Evaluation

Evaluation will be mostly based on theorem proving projects and/or paper presentations.