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 will be mostly based on theorem proving projects and/or paper presentations.