Journée LTP - Automne 2018

Co-localisée avec la journée MTV2

Cette page sera mise à jour régulièrement, n'hésitez pas à y revenir.

Date
jeudi 6 décembre 2018
Lieu
ENSIIE, Évry

Inscription avant le 19 novembre 2018

Cette journée est co-localisée avec la journée MTV2 (Méthodes de test pour la validation et la vérification), qui aura lieu le 7 décembre au même endroit.

Deux exposés invités seront présentés (résumés ci-dessous) :

Benoît Valiron (LRI/Modhel)
Calcul et langages de programmation quantique
Sylvain Boulmé (Laboratoire Verimag)
Embedding Impure ML Oracles into Coq Verified Code, Illustrated on SatAns-Cert, a Coq-Verified (Boolean) SAT-Solver.

Le GT LTP du GdR GPL :

Les thèmes du groupe de travail LTP (Langages, Types et Preuves) du GdR GPL sont :

Organisation

L'inscription à la journée est gratuite mais nécessaire pour assurer le bon déroulement de l'événement.

Le repas du midi n'est pas encore organisé, mais si tout se passe comme prévu, il sera financé par le GDR GPL.

Venir à l'ENSIIE

L'ENSIIE est facilement accessible depuis Paris Gare de Lyon ou Châtelet-Les halles via le RER D (gare d'Évry-Courcouronnes). Attention ne pas prendre les trains s'arrêtant à Évry Val de Seine, bien prendre ceux qui s'arrêtent à Évry-Courcouronnes. Sortez au bout du quai dans la direction du train. L'ENSIIE est ensuite fléchée.

Plus d'informations sur le site de l'ENSIIE.

Hôtels à proximité de l'ENSIIE (non testés, cette liste ne doit pas être considérée comme un soutien) :

Liste de participants

Présentations invitées

Sylvain Boulmé, Laboratoire Verimag

Embedding Impure ML Oracles into Coq Verified Code, Illustrated on SatAns-Cert, a Coq-Verified (Boolean) SAT-Solver.

Oracles are a key ingredient in the success of CompCert (an industrial C-Compiler which is formally verified in Coq). Such an oracle is an untrusted foreign code (written in OCaml) producing outputs that are checked by Coq-verified code. However, in CompCert, oracles are currently invoked through an unsafe FFI (Foreign Function Interface) of Coq. I will detail some pitfalls of this FFI and propose how to overcome them. Moreover, I conjecture that by using an adequate FFI, we can derive "theorems for free" a la Wadler in Coq from the ML type of imperative polymorphic oracles. This discharges a part of the proof effort on the OCaml typechecker. I will illustrate this idea on a few examples, including "SatAnsCert", a verified checker of boolean SAT-solvers.

Benoît Valiron, LRI/Modhel

Calcul et langages de programmation quantique

Dans cet exposé, je présenterai le calcul quantique, ses promesses, et l'état de l'art sur le front des langages de programmation quantique.

Programme

Le programme sera affiché ici.

Inscription

Envoyez votre inscription par e-mail à renaud.rioboo@ensiie.fr et guillaume.burel@ensiie.fr (cliquez ici, ou recopiez le bulletin ci-dessous) avant le 19 novembre.

Vous pouvez proposer des présentations de vos travaux sous la forme d'un exposé oral, d'un tutoriel, d'une démonstration d'outil, etc.

===================================
Nom :
Prénom :
Laboratoire/équipe :

[] je souhaite présenter des travaux.

 Titre et format de la présentation :

 Résumé (optionnel, à transmettre avant le 5/12) :

[] j'accepte que mes nom, prénom, équipe et éventuel titre de présentation
    apparaissent sur la page web de la journée, dès mon inscription.

[] je participerai au repas du midi.

 Pour le déjeuner, mes contraintes sont (végétarien, sans sel, ...) :

[] je participerai également à la journée MTV2 le lendemain.
   (pour information uniquement, l'inscription devra se faire des deux
    côtés.)

====================================