OUPS Mars 2023

Le prochain OUPS aura lieu le jeudi 16 mars 2023. Le rendez-vous est fixé à 19h au 4 place Jussieu en Amphi Astier dans le bâtiment Esclangon.
L'inscription est obligatoire pour pouvoir accéder au meetup !
Les exposés seront également retransmis en ligne sur le galène du OUPS.
Toutes les informations sont disponibles sur le site du OUPS.

Programme :

Deux moteurs de recherche pour l'ecosystème OCaml -- Arthur Wendling
Sherlocode et Sherlodoc sont deux petits outils pour explorer les nombreux projets publiés sur opam. Le premier permet de `grep` en temps réel leur code source, tandis que le second facilite la recherche dans leur documentation (à la Hoogle).
Durant la présentation, on verra que ces outils existent pour satisfaire deux envies : répondre à des questions tordues sur l'usage d'OCaml, mais aussi apprendre à coder ce type de moteur de recherche. On expliquera donc comment les recherches par regex et par type ont été implémentées, grâce à des astuces élégantes empruntées à la littérature... et des hacks douteux qu'il vaudrait mieux ne pas ébruiter.

Creusot a prophetic verifier for Rust -- Xavier Denis
Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strong ownership policy. This feature opens promising advances for deductive verification,
which aims at proving the conformity of Rust code with respect to
a specification of its intended behavior. We present Creusot, a tool for the formal specification and deductive verification of Rust. Creusot's specification language features a notion of prophecies to reason about memory mutation. Rust provides advanced abstraction features based on a notion of traits, extensively used in the standard library and in user code. The support for traits is at the heart of Creusot's approach of verification and specification of programs

***

Les présentations seront suivies par des discussions libres. Les pizzas seront offertes par la fondation OCaml !