3rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory
Victoria, British Columbia, Canada
- Session I: 9:00-10:30
- Formalizing an Extensional
Semantics for Units of Measure
Andrew Kennedy
Microsoft Research Cambridge
[slides]
Proving correctness of a dynamic
atomicity analysis in Coq
Caitlin Sadowski, Jaeheon Yi,
Kenneth Knowles, and Cormac Flanagan
University of California at
Santa Cruz
Mechanizing the Metatheory of a
Language With Linear Resources and Context Effects
Daniel K. Lee [1], Derek Dreyer
[2], and Andreas Rossberg [2]
[1] Carnegie Mellon University
[2] Max Planck Institute for
Software Systems
10:30-11:00 Break
Session II: 11:00-12:00
- Case Study: Subject Reduction
for Mini-ML with References, in
Isabelle/HOL + Hybrid
Alan J. Martin
University of Ottawa
[slides]
Mechanizing Methatheory with
Nested Datatypes
Andre Hirschowitz [1] and Marco
Maggesi [2]
[1] University of Nice (UNS) and
CNRS
[2] University di Firenze
12:00-14:00 Lunch
Session III: 14:00-15:00
- Shallow embedding of a logic in
Coq
Jerome Vouillon
Universite Paris Diderot - Paris
7, CNRS
[slides]
Names via Substructural and
Dependent Types
Jason Reed
Carnegie Mellon University
[slides]
15:00-15:30 Break
Session IV: 15:30-17:00
- SASyLF: An Educational Proof
Assistant for Language Theory
Jonathan Aldrich [1], Robert J.
Simmons [1], and Key Shin [2]
[1] Carnegie Mellon University
[2] Microsoft Corporation
[slides]
Building Verified Language Tools
in Operational Type Theory
Aaron Stump
The University of Iowa
[slides]
5-minute talks -