Changes between Version 1 and Version 2 of FraDeCoPP-2
- Timestamp:
- Nov 19, 2012, 6:09:13 PM (6 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
FraDeCoPP-2
v1 v2 1 = FraDeCoP 2012 --Workshop on Frameworks for the Development of Correct (parallel) Programs =1 = FraDeCoP-2 -- Second Workshop on Frameworks for the Development of Correct (parallel) Programs = 2 2 3 3 == Date and Location == 4 4 5 FraDeCoP will be held in Université Paris-Est Créteil, France on May 15th, 20126 7 Salle des thèses[[BR]]8 LACL, Bâtiment P2 du CMC,[[BR]]9 61 avenue du Général de Gaulle[[BR]]10 94010 Créteil Cedex[[BR]]11 Université de Paris-Est-Créteil12 13 [http://www.lacl.fr/en/venue]14 5 15 6 == Program == 16 7 17 10:00-10:30 Accueil [[BR]]18 [[BR]]19 10:30-11h15 Kiminori Matsuzaki : Constructive Algorithmic ([[http://tesson.julien.free.fr/research/FraDeCoPP/FraDeCoPP_Matsuzaki_Constructive_algorithmics.pdf|slides]])[[BR]]20 [[BR]]21 11:15-12:00 Julien Tesson : Mechanisation of constructive algorithmic with Coq ([[http://tesson.julien.free.fr/research/FraDeCoPP/FraDeCoPP_Tesson_constructive_algorithmics_in_coq.pdf |slides]])[[BR]]22 [[BR]]23 12:00-13:30 Lunch[[BR]]24 [[BR]]25 13:30-14:15 Matthieu Giorgino : Proofs of pointer algorithms by inductive representation of graphs ([#absgio abstract] | [[http://tesson.julien.free.fr/research/FraDeCoPP/FraDeCoPP_Giorgino_proof_of_pointer_algorithm.pdf| slides]])[[BR]]26 [[BR]]27 14:15-15:30 Vladimir Komendantsky : Cost analysis for patterns of parallelism ([#abskome abstract] | [[http://tesson.julien.free.fr/research/FraDeCoPP/FraDeCoPP_Komendantsky.pdf|slides]] )[[BR]]28 [[BR]]29 15:30-16:00 Coffee break[[BR]]30 [[BR]]31 16:00-16:45 Frédéric Gava : Verification of imperative BSP programs ([[http://tesson.julien.free.fr/research/FraDeCoPP/FraDeCoPP_Fortin_Gava_verif_imperative_bsp.pdf| slides]])[[BR]]32 [[BR]]33 16:45-18:00 Discussion / Démos [[BR]]34 [[BR]]35 8 == Abstracts == 36 9 37 [=#absgio]38 Mathieu 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 42 [=#abskom]43 Vladimir Komendantsky : Cost analysis for patterns of parallelism [[BR]]44 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]]45 [[BR]]46 10 47 11 == Aim and Scope == … … 70 34 71 35 * Experience feedback on the development of "formally proved correct" programs 72 73 74 == Talk Proposal ==75 76 To propose a talk for the workshop, please email Julien Tesson (tesson.julien_at_kochi-tech.ac.jp) before April 30, 2012, a title and a short abstract in plain text or pdf format.77 78 == Organiser ==79 80 Julien Tesson, Kochi University of Technology, Japan.[[BR]]81 Kiminori Matsuzaki, Kochi University of Technology, Japan.[[BR]]82 Frédéric Gava, Université Paris-est Créteil, France.83 84 85 == Registration ==86 87 Registration is free, but it is mandatory to do it before may 1st by sending an e-mail to Julien Tesson (tesson.julien_at_kochi-tech.ac.jp). [[BR]]88 Free lunch and coffee break, travel expenses may be reimbursed if needed (contact us as early as possible).
