Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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 ​
  
  
workshop_5.1404046247.txt.gz · Last modified: 2014/06/29 14:50 by paulin
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0