CS430/530: Formal Semantics, Fall 2013, Yale University

Here are a list of possible project ideas.
  1. 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.

  2. 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).

  3. 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.

  4. 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.

  5. 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.

  6. Interested in writing an essay? Here are a few thought-provoking papers or blogs: You can also browse recent papers in the top PL conferences, POPL, PLDI, SPLASH, and ICFP.

  7. Study more about first-class continuations (call/cc) (checkout the wikipedia page and also this page).

  8. Read the paper on Freefinement (PDF) and apply the idea to a different logic or type system and show what the resulting refinement system is like.

  9. Apply what you learned from this class to formalize some aspects of popular sci-fi movies (e.g., inception, source code).

Copyright (c) 2013 Zhong Shao, Dept. of Computer Science, Yale University