Séminaire CLAP - 16/12/21 - recherche par types et Coq SydPaCC
Vous êtes cordialement invités à participer au séminaire CLAP le 16 décembre 2021 de 10h15 à 11h40. Le séminaire se fera en visio sur zoom (info de connexion ci-dessous). Vous êtes également conviés à un café CLAP de 10h à 10h15 sur gather.town (https://gather.town/app/7giEyr3CTKAwe3Or/cafeCLAP)
Au programme :
- 10h20-11h00 : Fast Indexing for Research by Types par Gabriel Radanne
- 11h00-11h40 : Automated and Verified Algorithmic Skeleton-based Parallelization of Functional Programs par Frederic Loulergue
10h20-11h00 : Fast Indexing for Research by Types par Gabriel Radanne
We present a function retrieval system for OCaml. By combining unification modulo isomorphism and smart indexing techniques, it can efficiently manage a large database of libraries. In particular, A novel notion of feature allow to overcome in practice the efficiency limitations imposed by rich unification, as informed by metrics collected on concrete queries. This talk will present both practical and formal aspects of our tool for search by type, along with future plans.
11h00-11h40 : Automated and Verified Algorithmic Skeleton-based Parallelization of Functional Programs par Frederic Loulergue
SyDPaCC is a set of libraries for the Coq proof assistant. It allows to write naive functional programs (i.e. with high complexity) that are considered as specifications, and to transform them into more efficient versions. These more efficient versions can then be automatically parallelized before being extracted from Coq into source code for the functional language OCaml together with calls to the Bulk Synchronous Parallel ML (BSML) library.
For the optimization of sequential functions, SyDPaCC provides theorems such a the second homomorphism theorem that states that a homomorphic function is equivalent to a composition of map and reduce.
SyDPaCC also provides a set of algorithmic skeletons, programmed using BSML, and proved correct with respect to sequential functions. Algorithmic skeletons are higher-order function implemented in parallel, such as map and reduce but on distributed data structures. The way the correctness is stated is the basis of the automatic parallelization feature of SyDPaCC.
Sujet : Zoom meeting invitation - Séminaire CLAP
Heure : 16 déc. 2021 10:20 AM Paris
Participer à la réunion Zoom
ID de réunion : 868 5945 2604
Code secret : 710816
Une seule touche sur l’appareil mobile
+12532158782,,86859452604#,,,,*710816# États-Unis (Tacoma)
+13017158592,,86859452604#,,,,*710816# États-Unis (Washington DC)
Composez un numéro en fonction de votre emplacement
+1 253 215 8782 États-Unis (Tacoma)
+1 301 715 8592 États-Unis (Washington DC)
+1 312 626 6799 États-Unis (Chicago)
+1 346 248 7799 États-Unis (Houston)
+1 669 900 6833 États-Unis (San Jose)
+1 929 205 6099 États-Unis (New York)
ID de réunion : 868 5945 2604
Code secret : 710816
Trouvez votre numéro local : https://us02web.zoom.us/u/kcMmT9BtTM
Date:
Jeudi, 16 Décembre, 2021