Co-located with ICFP’10
| 8:00 - 8:45 | Continental breakfast | |
| 9:00 - 10:00 |
Andrew Appel (Princeton University)
Modular Foundational Verification of the Software Toolchain (Invited Talk) |
|
| 10:00 - 10:30 | Break | |
| 10:30 - 11:30 |
Christian Urban (TU Munich)
Nominal Isabelle or, How I learned to stop worrying and love the Variable Convention (Invited Talk) |
|
| 11:30 - 11:50 |
Yukiyoshi Kameyama (University of Tsukuba), Oleg Kiselyov (FNMOC),
Chung-chieh Shan (Rutgers University) Mechanizing multilevel metatheory with control effects |
|
| 11:50 - 12:10 |
James Cheney (University of Edinburgh) Mechanized metatheory: ready for prime time? |
|
| 12:10 - 12:30 |
Benoit Montagu (INRIA) Experience report: Mechanizing Core F-zip using the locally nameless approach |
|
| 12:30 - 2:00 | Lunch | |
| 2:00 - 3:00 |
Karl Crary (Carnegie Mellon University)
Mechanization of Full-Scale Languages (Invited Talk) |
|
| 3:00 - 3:30 | Break | |
| 3:30 - 4:30 |
Amy
Felty (University of Ottawa)
Reasoning with Higher-Order Abstract Syntax in Hybrid and Related Systems (Invited Talk) |
|
| 4:30 - 5:00 | Break | |
| 5:00 - 5:30 |
Steve Zdancewic (University of Pennsylvania)
Living with Locally Nameless (Invited Talk) |
|
| 5:30 - 6:00 |
Scott Owens and
Peter Sewell (University of Cambridge),
Stephanie Weirich (University of Pennsylvania),
Francesco Zappa Nardelli (INRIA) Ott Or Nott |