## Projects## CS430/530: Formal Semantics, Fall 2013, Yale University |

- 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.
- Formal Semantics for Top 5 Programming Languages
- Featherweight Java
- The Essence of JavaScript
- Mini-JavaScript (a.k.a. CoreScript)
- Pyton: The Full Monty

- 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:
- William Cook's paper on On understanding data abstraction, revisited and his related blog post; also see Jonathan Aldrich's latest essay.
- Guy Steele's paper on Growing a Language (also see the talk by the author on youtube)
- Harper's Blog including a few interesting pieces (1, 2, 3))
- Dijkstra's EWD Archive
- Lambda the Ultimate, the PL weblog

- Study more about first-class continuations (call/cc)
(checkout the wikipedia page and also this page).
- 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.
- 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