The next OUPS meetup will take place on Thursday, 16th of March 2023. It will start at 7pm at the 4 place Jussieu, 75005 Paris.
It will be in the in the Astier amphitheater in the Esclangon building.
Please, register on meetup as soon as possible to let us know how many pizza we should order.
For more details, you may check the OUPS’ website .
This month will feature the following talks :
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