The next OUPS meetup will take place on Thursday, 11th of May 2023. It will start at 7pm at the 4 place Jussieu in Paris.
It will be in the in the Herpin 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 :
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 (@Armael)
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.
