OUPS Mai 2023

Le prochain OUPS aura lieu le jeudi 11 mai 2023. Le rendez-vous est fixé à 19h au 4 place Jussieu en Amphi Herpin 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 :

Retrofitting OCaml Modules -- Clément Blaudeau
ML modules offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, and more recent extensions (abstract signatures, module aliases) lack a complete formalization. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a significant subset of OCaml modules, including both applicative and generative functors and transparent ascription -- a useful new feature. By exploring the translations both to and from Fω, we provide a complete description of the signature avoidance issue, as well as insights on the limitations and benefits of the path-based approach of OCaml type-sharing.

Formal reasoning rules for the OCaml FFI -- Armaël Guéneau
OCaml provides an FFI mechanism (Foreign Function Interface) allowing
OCaml programs to call external functions implemented in C, typically by
writing "glue code" helping bridge the two languages. This "glue code"
needs to be carefully written and obey a number of rules when
interacting with the OCaml runtime (cf chapter 22 of the manual).
Failure to follow one of these rules typically result in silent corruption of the program memory, resulting in fatal and hard to debug
crashes.
This presentation will present ongoing research on formalizing the
rules one need to follow to correctly use the OCaml FFI. We will see how
a small number of permissions can capture the requirements one must
obey in order to write bug-free glue code.

***

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