CS430/530: Formal Semantics, Fall 2013, Yale University
Here are a list of possible project ideas.
If you have some cool ideas you want to pursue, even if it is
a bit vague, come to talk to the instructor and/or the TA. We can
probably refer you to related papers and previous work.
Pick some language and its semantics in Harper's or Reynolds'
textbooks and implement it in Coq. Prove some simple soundness
properties (e.g., safety).
Pick a tiny subset of your favorite programming language
(here is a complete list)
and write
its static and/or dynamic semantics (and as a bonus, prove type safety).
Here are some earlier examples in our field that have resulted in influential publications.
Read Reynolds' lecture notes on
separation logic. Work on a subset of its
exercises in Chapters 4 and 5, or apply separation logic to verify
some favorite algorithm (and data structure) implementation.
Read those chapers (in the
Software
Foundations book) which we did not
have time to cover during our lecture. Solve some of those exercieses with
a difficult rating of 4 or 5.
Interested in writing an essay? Here are a few thought-provoking papers or blogs:
