Changes between Version 12 and Version 13 of FraDeCoPP2012


Ignore:
Timestamp:
May 5, 2012, 11:18:31 AM (6 years ago)
Author:
julien.tesson@…
Comment:

Planning

Legend:

Unmodified
Added
Removed
Modified

  • FraDeCoPP2012

    v12 v13  
    1515== Program == 
    1616 
    17 TBA 
     1710:00-10:30  Accueil [[BR]] 
     18[[BR]] 
     1910:30-11h15  Kiminori Matsuzaki : Constructive Algorithmic[[BR]] 
     20[[BR]] 
     2111:15-12:00  Julien Tesson : Mechanisation of constructive algorithmic with Coq[[BR]] 
     22[[BR]] 
     2312:00-13:30  Lunch[[BR]] 
     24[[BR]] 
     2513:30-14:15  Matthieu Giorgino : Proofs of pointer algorithms by inductive representation of graphs ([#absgio abstract])[[BR]] 
     26[[BR]] 
     2714:15-15:30  Vladimir Komendantsky : Cost analysis for patterns of parallelism ([#abskome abstract])[[BR]] 
     28[[BR]] 
     2915:30-16:00 Coffee break[[BR]] 
     30[[BR]] 
     3116:00-16:45 Frédéric Gava : Verification of imperative BSP programs [[BR]] 
     32[[BR]] 
     3316:45-18:00 Discussion / Démos [[BR]] 
     34[[BR]] 
     35== Abstracts == 
     36 
     37[=#absgio] 
     38Mathieu Giorgino : Proofs of pointer algorithms by inductive representation of graphs [[BR]] 
     39 We present a proof method based on the representation of pointer structures as inductive algebraic data-types adorned with additional pointers in a proof-assistant. The advantage is then to be able to apply structural induction principles and other usual techniques available in proof-assistant. We illustrate it on two case-studies: the verification of an algorithm to construct BDDs (Binary Decision Diagrams) and the verification of the Schorr-Waite algorithm.[[BR]]  
     40[[BR]] 
     41 
     42Vladimir Komendantsky : Cost analysis for patterns of parallelism [[BR]] 
     43 Several notions of cost analysis have been introduced in the literature for functional programs that produce structured (a.k.a. shapely) data. Departing from pure data, I propose a higher-order cost analysis for pattern matching programs (skeletons) that produce functional programs. The proposal employs the pattern matching calculus due to Barry Jay. I will illustrate the idea on a divide-and-conquer pattern implementation in that calculus.[[BR]] 
     44[[BR]] 
    1845 
    1946== Aim and Scope ==