Jules Chouquet

Publications

Conférences internationales

• Kostia Chardonnet, Jules Chouquet et Axel Kerinec (FSCD 2026) :
  Approximation theory for distant Bang calculus — (HTML) (pdf)
  Abstract

  Approximation semantics capture the observable behaviour of {\lambda}-terms, with Böhm Trees and Taylor Expansion standing as two central paradigms. Although conceptually different, these notions are related via the Commutation Theorem, which links the Taylor expansion of a term to that of its Böhm tree. These notions are well understood in Call-by-Name {\lambda}-calculus and have been more recently introduced in Call-by-Value settings. Since these two evaluation strategies traditionally require separate theories, a natural next step is to seek a unified setting for approximation semantics. The Bang-calculus offers exactly such a framework, subsuming both CbN and CbV through linear-logic translations while providing robust rewriting properties. However, its approximation semantics is yet to be fully developed. In this work, we develop the approximation semantics for dBang, the Bang-calculus with explicit substitutions and distant reductions. We define Böhm trees and Taylor expansion within dBang and establish their fundamental properties. Our results subsume and generalize Call-By-Name and Call-By-Value through their translations into Bang, offering a single framework that uniformly captures infinitary and resource-sensitive semantics across evaluation strategies.

• Jordan Ischard, Frederic Dabrowski, Jules Chouquet, and Frédéric Loulergue (SAC 2025) :
  A Mechanized Formalization of an FRP Language with Effects
  Abstract

  Functional Reactive Programming (FRP) is a functional programming paradigm designed for systems interacting with their environment. The Yampa library, a Haskell implementation, allows users to construct signal functions that synchronously process input streams to produce output streams. While this library facilitates concise and robust coding, managing I/O is cumbersome. To address this issue, the Wormholes library extends Yampa with constructs to bind I/O to resource names, accessible in an imperative style. Few FRP languages are formalized, and Wormholes added challenging features. This article presents a mechanized formalization of a slightly modified version of Wormholes, improving the result and correcting some issues.

• J.Chouquet et C.Tasson (CSL 2020) :
  Taylor expansion for Call-By-Push-Value
  Abstract

  Nous proposons un calcul à ressources adapté à Call-By-Push-Value, à l’aide duquel nous définissons un développement de Taylor. On établit que ce développement est cohérent avec les sémantiques opérationelles et dénotationelles de Call-By-Push-Value en nous inspirant d’outils de la Logique Linéaire. L’essentiel de ce travail consiste à donner une contrepartie syntaxique aux morphismes de coalgèbre de la sémantique.

• J. Chouquet (MFPS 2019) :
  Taylor expansion, finiteness and strategies
  Abstract

  On examine des méthodes récentes visant à étendre les résultats de Ehrhard et Regnier sur le développement de Taylor : les combinaisons linéaires d’approximants d’un λ-terme peuvent être normalisées sans faire apparaître de coefficients infinis. Les méthodes considérées permettent d’étendre ce résultat à des calculs non uniformes; on montre qu’en se concentrant sur des stratégies d’évaluation précises, comme l’Appel-Par-Valeur, l’Appel-Par-Nécessité, PCF, ou des variantes de l’Appel-Par-Pousse-Valeur (le Bang-Calcul en particulier), l’extension des résultats de finitude de Ehrhard et Regnier peuvent s’appliquer ou non, selon la structure du calcul original. En particulier, on introduit un calcul à ressources pour l’Appel-Par-Nécessité, et montrons que le résultat de finitude de son développement de Taylor peut être dérivé de nos considérations sur l’Appel-Par-Valeur. Nous introduisons aussi un calcul à ressources pour une présentation de PCF avec un point fixe explicite, et montrons comment cela interfère avec le résultat de finitude. On examine ensuite le Bang-Calcul de Ehrhard et Guerrieri, qui possède les propriétés de l’Appel-Par-Pousse-Valeur dans une présentation légèrement différente.

• J. Chouquet et L. Vaux-Auclair (CSL 2018) :
  An application of parallel cut elimination in unit-free multiplicative linear logic to the Taylor expansion of proof nets
  Abstract

  Nous étudions l'élimination des coupures parallèle dans les réseaux de preuve connexes de la logique linéaire multiplicative. Nous donnons une borne à la réduction de la taille et à l'évolution de la longueur des chemins d'interrupteurs sous réduction parallèle, et nous montrons que que ce résultat combinatoire s'applique au développement de Taylor des réseaux de MELL: les coefficients restent finis sous réduction de combinaisons linéaires infinies de réseaux à resource, car ces réseaux se comportent essentiellement comme ceux de MLL.

Articles

• J. Chouquet et L. Vaux-Auclair :
  An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets
  Abstract

  Nous étendons le résultat de notre article CSL, le généralisant à un fragment plus large de la logique linéaire, incluant les affaiblissements et les unités multiplicatives. Cela exige des méthodes spécifiques pour travailler avec les structures non connexes, en particulier à cause de coupures qui peuvent se réduire dans des sous-structures vides.

Thèse

• Une géométrie du calcul (en français). Soutenue le 6 décembre 2019.
• Transparents de la présentation.

Transparents d'exposés

• Sémantiques dénotationelles des programmes réactifs Présentation aux journées d'équipe LMV d’approches dénotationnelles de la programmation réactive, et pistes pour le projet de recherche associé.
• Topological insights on probabilistic agreement Presentation de resultats sur la topologie combinatoire appliquée aux algorithmes distribués probabilistes. Invitation au séminaire Verimag à Grenoble, février 2020.
• Taylor expansion for Call-By-Push-Value Présentation de l’article publié à CSL 2020, coécrit avec Christine Tasson.
• Ma vie, mon œuvre Presentation à la journée de rentrée de l’UFR d’informatique de l’Université de Paris. Septembre 2019.
• Elimination des coupures dans le développement de Taylor des réseaux. Présentation aux journées PPS de 2018
• Chemins et sauts dans le développement de Taylor des réseaux Présentation à l'atelier "Réseaux" du GDR Logique Linéaire à Villetaneuse, 2018
• Taylor expansion, finiteness and strategies Presentation de mon article à MFPS 2019 , Londres, 7 juin