This website presents the articles presented at the JFLA 2023. The conference website contains information about the event itself.

The full proceedings is also available as a single pdf.

The JFLA bring together designers, users, and theoreticians. The goal is to cover all areas of functional languages, from formal proofs, to program verification, and the mathematical objects that underlie these tools. These domains should be interpreted broadly: we hope to bridge between different themes.

• Functional languages and applications: semantics, compilation, optimisation, type systems, mesures, extensions to other paradigms.
• Proof assistants: implementations, new tactics, developments that are interesting from a technical or methodological point of view.
• Logic, the Curry-Howard Isomorphism, realisability, program extraction, models.
• Specification, prototyping, formal development of algorithms.
• Verification of programs or models, deductive methods, abstract interpretation, refinements.
• Industrial use of functional languages, or methods arising from formal proof, tools for the web.

Invited Talks

• À propos de l'agrégation d'informatique, Sylvie Boldo.
• Théorie et pratique des effets en OCaml 5, Xavier Leroy.

Invited Course

• Tutoriel Mathematical Components, Cyril Cohen.

Long Articles

• Effectful programming across heterogeneous computations — Work in progress, Jean Abou Samra, Martin Bodin, and Yannick Zakowski.
• Filtrer sans s'appauvrir : Inférer les paramètres constants des modèles réactifs probabilistes, Guillaume Baudart, Grégoire Bussone, Louis Mandel, and Christine Tasson.
• An AST for representing programs with invariants and proofs, Guillaume Bertholon and Arthur Charguéraud.
• Retrofitting OCaml modules: Fixing signature avoidance in the generative case, Clément Blaudeau, Didier Rémy, and Gabriel Radanne.
• Analyse de dépendance vérifiée pour un langage synchrone à flot de données, Timothy Bourke, Basile Pesin, and Marc Pouzet.
• Formal proofs applied to system models, Évelyne Contejean and Andrei Samokish.
• Do CPS translations also translate realizers?, Samuel Gardelle and Étienne Miquey.
• Building CFA for λ-calculus from Skeletal Semantics, Thomas Jensen, Vincent Rébiscoul, and Alan Schmitt.
• Traduire l'univers des mathématiques en Dedukti, sans univers, Amélie Ledein and Elliot Butte.
• Backtracking reference stores, Gabriel Scherer.
• Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs, Milla Valnet, Raphaël Monat and Antoine Miné.
• Vérification symbolique de protocoles cryptographiques en F* : application au sous-protocole TreeSync de MLS, Théophile Wallez.

Cour Articles

• Comment dompter un troupeau de flottants sauvages ?, Arthur Correnson.
• L'arithmétique de séparation, Jean-Christophe Filliâtre and Andrei Paskevich.

Prototype Demonstrations

• Goose: an OCaml environment for quantum computing, Denis Carnier, Arthur Correnson, Christopher McNally, and Youssef Moawad.
• Décision de relations inductives pour SMTCoq, Louise Dubois de Prisque.
• Caractériser des propriétés de confiance d'IA avec Why3, Julien Girard-Satabin, Michele Alberti, François Bobot, and Zakaria Chihani.
• Necro ML: Kit de Nécromancie, Louis Noizet and Alan Schmitt.