Peio Borthelle

About

I am currently a post-doctoral researcher in the Pascaline team of the LIP laboratory, at the ENS de Lyon. Before that I was a PhD student in the LIMD team of the LAMA at the USMB (Chambéry).

I am most happy hacking inside proof assistants or anything related type theory. My research interests include type theory, operational and denotational semantics, effects, syntax, game semantics and coinduction.

Email

peio.borthelle@inria.fr

Github

@lapin0t

ORCID

0009-0006-7733-7439

News

Papers

• An Abstract, Certified Account of Operational Game Semantics

  Conference paper — ESOP 2025

  Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski

  doipdfrocqartifact report

  Comment

  In this paper we present the main result we worked on during my PhD, namely the Rocq formalization of a language-generic operational game semantics model. We prove it sound w.r.t. a variant of contextual equivalence. To this end, we introduce a lightweight axiomatization of programming languages with operational semantics. The syntax is kept opaque and only required to support substitution, while the operational semantics is axiomatized as an automaton structure compatible with substitution. The model construction and soundness theorem can be instanciated with untyped and simply-typed higher-order languages featuring arbitrary control effects (such as non-termination or call/cc).

  A notable limitation is that our axiomatization does not cover any other kind of effects (such as state), although we hope to extend the construction to capture this with (substantial) further work.

• Operational Game Semantics in Type Theory

  PhD thesis — Université Savoie Mont Blanc

  Peio Borthelle

  nntpdfslidessource

  Comment

  In my PhD manuscript I try demystify operational game semantics (OGS) and normal-form bisimulations for the type theorist. Both of these are flexible frameworks for denotational semantics based on dialog trees (“game strategies”), defined in terms of a given operational semantics. The main results are as follows.

  • A presentation of Levy & Staton games and a construction of their sets of strategies as coinductive trees (more specifically as a dependently-typed variant of interaction trees).
  • A lightweight axiomatization of languages with an operational semantics presented as an kind of LTS, dubbed language machines.
  • A generic construction of an OGS and normal-form bisimulation model given any language machine.
  • A soundness proof for these two generic models w.r.t. a variant of CIU-equivalence (a flavor of observational/contextual equivalence).
  • Detailled examples of three language machines for jump-with-argument, polarized µµ̃-calculus and pure untyped call-by-name λ-calculus.

  It also contains a little proof pearl on intrinsically typed and scoped representations of syntax with binders that I’m quite happy with and which I didn’t see anywhere else.

• A Cellular Howe Theorem

  Conference paper — LICS 2020

  Peio Borthelle, Tom Hirschowitz, Ambroise Lafont

  doipdf

  Comment

  This paper builds upon work that I did during my master’s internship with Tom Hirschowitz. It provides a language-generic account for Howe’s method, a syntactic method for proving that applicative bisimilarity is a congruence (i.e., closed under context application). The categorical setting of the language-generic result builds on Fiore et al.‘s notion of Σ-monoid, with the programming language specified as a two-layer signature, first for generating the syntax of terms and then for generating the “syntax” of the reduction relation.

Talks

• Operational Game Semantics formally: Let’s talk about chattering

  Workshop talk — GALOP 2025

  Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski

  abstractslides

  Comment

  An ongoing-work talk about the OGS formalization in my PhD. The focus of the talk was on a novel decomposition of the standard but quite subtle coinductive soundness proof of OGS into a unicity of fixed points argument. This isolates the high-level proof from the technical justification and sheds some light on a previously poorly understood technical oddity of the OGS soundness proof.

• Games and Strategies using Coinductives Types

  Workshop talk — TYPES 2023

  Peio Borthelle, Tom Hirschowitz, Guilhem Jaber, Yannick Zakowski

  abstractslidesvideo

  Comment

  An ongoing-work talk about the OGS formalization in my PhD. The focus of the talk was on a simple notion of game by Levy & Staton, and how it relates to interaction trees and to greatest fixed points of indexed polynomial functors.

Miscellaneous

• Will we continue scientific research?

  CERN talk — January 1972

  Alexandre Grothendieck, translation by Peio Borthelle

  transcriptionaudio

  Comment

  A translated transcription of the 1972 CERN talk and debate by mathematician Alexandre Grothendieck. He first lays out his harsh critic of the modern scientific institution, underlining still very relevant problems related to personal motivations, pleasure and well-being at work. The debate then goes on to clarify several points of his positions.

• Deriving an Induction Principle for Church Numerals

  Unpublished formalization

  Peio Borthelle

  htmlsource

  Comment

  A little experiment in litterate Rocq (rendered using Alectryon). It has been proven that in several standard type theories, one cannot obtain an induction principle on Church-encoded data types. Yet as we will see, this is not true in the presence of a universe of strict propositions.