Registration
This shows you the differences between two versions of the page.
|
workshop_5 [2014/06/29 14:50] paulin [Lectures and abstract] |
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 | | ||
| |14h00-14h45 |Brigitte Pientka |Programming logical relations proofs | | |14h00-14h45 |Brigitte Pientka |Programming logical relations proofs | | ||
| - | |14h45-15h30 |Tarmo Uustalu |Precise qualification of effects with dependently typed monads | | + | |14h45-15h45 |Arthur Charguéraud |Interactive verification of stateful higher-order programs using characteristic formulae | |
| - | |16h00-17h00 |Arthur Charguéraud |Interactive verification of stateful higher-order programs using characteristic formulae | | + | |
| ^ Tuesday 8 July ^^^ | ^ Tuesday 8 July ^^^ | ||
| |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 |Martin Hofmann |Abstract effects and proof-relevant logical relations | | + | |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 33: | 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 | | ||
| Line 43: | Line 43: | ||
| |16h30-17h30| Peter Sewell |Before Certification: Engineering Validatable Models | | |16h30-17h30| Peter Sewell |Before Certification: Engineering Validatable Models | | ||
| ^ Friday 11 July ^^^ | ^ Friday 11 July ^^^ | ||
| - | |09h30-10h30|Nick Benton-Andrew Kennedy |Generating Certified x86 Code in a Proof Assistant | | + | |09h00-10h00| Nick Benton-Andrew Kennedy |Generating Certified x86 Code in a Proof Assistant | |
| - | |11h00-11h45|Adam Chlipala |Bedrock: A Foundational Proof-Carrying Code Platform with Functional Correctness Proofs | | + | |10h00-10h45| Adam Chlipala |Bedrock: A Foundational Proof-Carrying Code Platform with Functional Correctness Proofs | |
| - | |11h45-12h30|Dan Ghica |Compiling functional programs to distributed architectures using abstract machine nets | | + | |11h15-12h00| Dan Ghica |Compiling functional programs to distributed architectures using abstract machine nets | |
| + | |12h00-12h45| Martin Hofmann |Abstract effects and proof-relevant logical relations | | ||