Registration
This shows you the differences between two versions of the page.
workshop_5 [2014/06/30 08:06] paulin [Planning] |
workshop_5 [2014/07/03 18:25] (current) paulin [Planning] |
||
---|---|---|---|
Line 18: | Line 18: | ||
===== Planning ===== | ===== Planning ===== | ||
^ Monday 7 July ^^^ | ^ Monday 7 July ^^^ | ||
- | |09h30-10h30 | |Registration and Introduction | | + | |09h30-10h30 | Registration and Introduction || |
|10h30-11h30 |Andreas Abel |Coinduction in Agda using Copatterns and Sized Types | | |10h30-11h30 |Andreas Abel |Coinduction in Agda using Copatterns and Sized Types | | ||
|11h30-12h15 |Stephanie Weirich |Combining Proofs and Programs in a Dependently Typed Language | | |11h30-12h15 |Stephanie Weirich |Combining Proofs and Programs in a Dependently Typed Language | | ||
Line 26: | Line 26: | ||
|09h30-10h30 |Nobuko Yoshida |Idioms for Interaction and their applications in large distributed systems | | |09h30-10h30 |Nobuko Yoshida |Idioms for Interaction and their applications in large distributed systems | | ||
|11h00-11h45 |Tarmo Uustalu |Precise qualification of effects with dependently typed monads | | |11h00-11h45 |Tarmo Uustalu |Precise qualification of effects with dependently typed monads | | ||
- | |11h45-12h30 |Greg Morrisett |Engineering Challenges for Modeling Languages | | + | |11h45-12h30 |Greg Morrisett |Engineering Challenges for Modeling Languages (cancelled) | |
^ Wednesday 9 July ^^^ | ^ Wednesday 9 July ^^^ | ||
|09h30-10h30 |Amal Ahmed |Compositional Compiler Verification for a Multi-language World | | |09h30-10h30 |Amal Ahmed |Compositional Compiler Verification for a Multi-language World | | ||
Line 32: | Line 32: | ||
|11h45-12h30 |David Pichardie |Atomicity Refinement for Verified Compilation | | |11h45-12h30 |David Pichardie |Atomicity Refinement for Verified Compilation | | ||
|14h30-15h15 |Steve Zdancewic |Vellvm: Verifying Transformations of the LLVM IR | | |14h30-15h15 |Steve Zdancewic |Vellvm: Verifying Transformations of the LLVM IR | | ||
- | |15h15-16h00 |Francesco Zappa-Nardelli |Concurrency and compiler correctness | | + | |15h15-16h00 |Francesco Zappa-Nardelli |Concurrency: Still Tricky | |
|16h30-17h30 |Xavier Leroy |Verified static analyses | | |16h30-17h30 |Xavier Leroy |Verified static analyses | | ||
+ | |18h00| Cocktail || | ||
^ Thursday 10 July ^^^ | ^ Thursday 10 July ^^^ | ||
|09h30-10h30| Derek Dreyer |GPS: Navigating weak memory with ghosts, protocols, and separation | | |09h30-10h30| Derek Dreyer |GPS: Navigating weak memory with ghosts, protocols, and separation | |