Meetup OUPS (OCaml Users in PariS) : le passĂ© đȘ
Les vidéos des meetups OUPS passés sont disponibles ici !
Mai 2023 Mars 2023 Janvier 2023 DĂ©cembre 2022 Septembre 2022 Mai 2022 Mars 2022 DĂ©cembre 2021
Les vidéos des meetups OUPS passés sont disponibles ici !
Mai 2023 Mars 2023 Janvier 2023 DĂ©cembre 2022 Septembre 2022 Mai 2022 Mars 2022 DĂ©cembre 2021
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.
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.
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
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.
Afin de prĂ©venir les erreurs de programmation, des analyseurs statiques ont Ă©tĂ© dĂ©veloppĂ©s pour de nombreux langages ; cependant, aucun analyseur mature ne cible lâanalyse de valeurs pour un langage fonctionnel Ă la ML. On dĂ©crira ici un analyseur statique de valeurs par interprĂ©tation abstraite pour un langage fonctionnel typĂ© du premier ordre, approche sĂ»re et automatique pour garantir lâabsence dâerreurs Ă lâexĂ©cution. Cette approche nous permet dâanalyser des fonctions rĂ©cursives manipulant des types algĂ©briques rĂ©cursifs et dâinfĂ©rer dans un domaine abstrait leur relation entrĂ©e-sortie. Une implĂ©mentation est en cours sur la plateforme MOPSA et analyse avec succĂšs de courts programmes de quelques lignes. Ce travail ouvre ainsi la voie vers une analyse de valeurs prĂ©cise et relationnelle basĂ©e sur lâinterprĂ©tation abstraite pour les langages fonctionnels dâordre supĂ©rieur Ă la ML.
YOCaml est un générateur de blog statique qui a été développé pour tester la bibliothÚque Preface. Il est relativement peu pragmatique, partiellement mal documenté et ne dispose d'aucune stratégie de mise en cache efficace. Cependant, sa genÚse est amusante (et tùche d'utiliser des outils peu présents dans le monde de OCaml) et certaines contributions extérieures ont permis de le rendre assez explicitement couplable avec MirageOS. Dans cette présentation, je vous propose de découvrir son fonctionnement général, quelques choix de design et un bref tutoriel sur comment l'utiliser.
In this talk, I will present Camlboot, a project which debootstraps the OCaml compiler, that is, is able to compile the OCaml compiler without using the bootstrap binary. Camlboot consists in a naĂŻve compiler for a subset of OCaml called MiniML, and an interpreter for OCaml written in MiniML. I will first justify the interest of debootstrapping, then explain the architecture and parts of Camlboot, and finally present the experimental validation of Camlboot.
Cette présentation sera une introduction informelle et simpliste à la programmation musicale via un ordinateur. Il existe de nombreux langages de "live coding" (SonicPi, TidalCycles), mais il est aussi tout à fait possible d'expérimenter de s'amuser avec notre langage favori! Je présenterai divers projets sur lesquels j'ai expérimenté, avec des démonstrations sonores en accompagnement. Avertissement: cette présentation contient des compliments au protocole MIDI.
COBOL est un langage trĂšs ancien et est assez Ă©loignĂ© de ceux que nous manipulons tous les jours. MalgrĂ© cela il reste lâun des plus utilisĂ©s dans le monde. Durant cette prĂ©sentation je vais donc vous introduire au langage, voir comment sont Ă©crit les programmes, comment les variables sont-elles dĂ©clarĂ©es et comment les manipuler. Je vais aussi vous prĂ©senter quelques features âintĂ©ressantesâ du langage, dont certaines sont inattendues.
OCaml 5.0 est la premiÚre nouvelle version majeure d'OCaml en dix ans d'évolution du langage. Cette nouvelle version majeure dénote une réécriture presque totale de l'environnement d'exécution afin de supporter deux nouveautés majeures: le parallélisme et les effets algébriques. Mon exposé propose de faire un tour de ces nouvelles fonctionnalités du langage, mais aussi de présenter le travail accompli pour préserver la compatibilité avec tout le code OCaml existant.
Lâutilisation dâun gestionnaire de paquets sources comme Opam nâest pas toujours optimale en temps, car lâoutil passe beaucoup de temps Ă recompiler des paquets, dĂšjĂ compilĂ©s dans le passĂ© ou par dâautres utilisateurs. Le plugin Opam-bin rĂ©pond Ă ce problĂšme en permettant de crĂ©er Ă la volĂ©e des paquets binaires, qui seront rĂ©utilisĂ©s Ă lâavenir et peuvent ĂȘtre partagĂ©s avec dâautres utilisateurs. LâexposĂ© montre son utilisation et comment il fonctionne.
Gospel is a behavioural specification language for OCaml program. It provides developers with a non-invasive and easy-to-use syntax to annotate their module interfaces with formal contracts that describe type invariants, mutability, function pre-conditions and post-conditions, effects, exceptions, and much more!
MirageOS 4 vient de sortir récemment et c'est l'occasion de (re)présenter ce projet permettant de construire des unikernels. Nous y présenterons les nouvelles features et possibilités et nous ferons une introspection de 3 ans de travail de l'équipe core.
Tezt is a test framework for OCaml. It is well suited for unit and regression tests and particularly shines for integration tests, i.e. tests that launch external processes. It was made with a focus on user experience. It allows you to easily select tests from the command-line and provides pretty logs. It also can run tests in parallel, automatically split the set of tests into several well-balanced batches to be run in parellel CI jobs, produce JUnit outputs, and more. It has been in use at Nomadic for the last 2 years and is thus quite battle-tested.
Sundials/ML is an OCaml interface to (most of) the Sundials suite of numerical solvers. It provides access to the underlying C library and exploits features of the OCaml type and module systems to document and ensure its correct utilisation. We reimplemented a hundred-odd of the examples provided with Sundials to aid in developing, debugging, and benchmarking the OCaml library. The standard examples, iterated hundreds or thousands of times, are rarely twice as slow in OCaml as in C and usually less than 50% slower. We also found many bugs in our code (and a few in Sundials itself) by executing these examples with valgrind.
OCaml is a great choice for simulating mathematical models: Its functional nature and its type and module system allow to easily express mathematical models and to simulate them in a modular and (reasonably) efficient manner. I will share some of the code and results from my PhD about the Bayesian inference of infectious diseases, with simulation of stochastic processes, MCMC, phylogenetic inference, and musical populations.
In this talk, I will give a brief presentation and demo of Monolith, a tool that helps apply random testing or fuzz testing to an OCaml library. Monolith provides a rich specification language, which allows the user to describe her libraryâs API, and an engine, which generates clients of this API and executes them. This reduces the problem of testing a library to the problem of testing a complete program, one that is effectively addressed by off-the-shelf fuzzers such as AFL.
La conception de molĂ©cules par ordinateur est un sujet qui revient Ă la mode. Pour gĂ©nĂ©rer in-silico des molĂ©cules aux propriĂ©tĂ©s optimisĂ©es, une fonction de score peut ĂȘtre couplĂ©e Ă un gĂ©nĂ©rateur molĂ©culaire. Nous allons montrer une mĂ©thode simple qui permet de gĂ©nĂ©rer uniquement des molecules valides, Ă haute frĂ©quence. Le logiciel libre FASMIFRA implĂ©mente cette mĂ©thode en OCaml.
Durant cette prĂ©sentation, nous vous emmĂšnerons visiter les profondeurs dâOCaml. Vous y dĂ©couvrirez comment Ă©crire du code lorsque votre seul objectif est dâĂ©viter les allocations. Ă condition bien Ă©videmment de ne pas craindre la honte. Vous pourrez Ă©galement apercevoir de vĂ©ritables morceaux de flambda et de futurs vĂ©ritables morceaux de flambda2.