This website presents the articles presented at the JFLA 2022. All of them have been uploaded to HAL. The conference website contains information about the event itself.

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 rpograms or models, deductive methods, abstract interpretation, refinements.
• Industrial use of functional languages, or methods arising from formal proof, tools for the web.

Table of Contents

Long Articles

• Inférence parallèle pour un langage réactif probabiliste, Guillaume Baudart, Louis Mandel, Marc Pouzet et Reyyan Tekin.
• Formalisation d'un vérificateur efficace d'assertions arithmétiques à l'exécution, Thibaut Benjamin, Félix Ridoux et Julien Signoles.
• Vers une traduction de K en Dedukti, Valentin Blot, Catherine Dubois et Amélie Ledein.
• Un Coq apprend à un bébé colibri à flotter, François Bobot et Arthur Correnson.
• Hydras & Co.: Formalized mathematics in Coq for inspiration et entertainment, Pierre Castéran, Jérémy Damour, Karl Palmskog, Clément Pit-Claudel et Théo Zimmermann.
• Macle : un langage dédié à l'accélération de programmes OCaml sur circuits FPGA, Emmanuel Chailloux, Jocelyn Sérot et Loïc Sylvestre.
• Déboîter les constructeurs, Nicolas Chataing, Camille Noûs et Gabriel Scherer.
• Inférer et vérifier les tailles de tableaux avec des types polymorphes, Jean-Louis Colaço, Baptiste Pauget et Marc Pouzet.
• Formalising Futures et Promises in Viper, Cinzia Di Giusto, Loïc Germerie Guizouarn, Ludovic Henrio et Etienne Lozes.
• A reactive operational semantics for a lambda-calculus with time warps, Adrien Guatto, Christine Tasson et Ada Vienot.

Short Articles

• Connecter l'écosystème OCaml à Software Heritage via opam, Léo Andrès, Raja Boujbel, Louis Gesbert et Dario Pinto.
• Alt-Ergo-Fuzz: A fuzzer for the Alt-Ergo SMT solver, Guillaume Bury, Steven de Oliveira et Hichem Rami Ait El Hara.

Prototype Demonstrations

• Bécassine à la chasse au Coq, Valentin Blot, Louise Dubois de Prisque, Chantal Keller et Pierre Vial.
• Jouez à Faire Consensus Avec Mitten!, Çagdas Bozman, Mohamed Iguernlala, Michael Laporte, Maxime Levillain, Alain Mebsout et Sylvain Conchon.
• Soyez prudent : prenez des photos pour l'assurance avec osnap, Valentin Chaboche, Zaynah Dargaye et Arvid Jakobsson.
• Mikino: Induction for Dummies, Adrien Champion, Steven de Oliveira et Keryan Didier.
• Trakt : Uniformiser les types pour automatiser les preuves, Denis Cousineau, Enzo Crance et Assia Mahboubi.
• Catala, un langage pour transformer la loi en code, Alain Delaet et Denis Merigoux.
• Actema: une interface graphique et gestuelle pour preuves formelles, Pablo Donato, Pierre-Yves Strub et Benjamin Werner.
• Démonstration de Steel, une logique de séparation concurrente pour prouver des programmes F*, Aymeric Fromherz et Antonin Reitz.
• Number Notation dans Coq, Pierre Roux.

Program Committee