Peio Borthelle
I am currently a PhD student, under the supervision of Tom Hirschowitz, Guilhem Jaber and Yannick Zakowski. I am located at Université Savoie Mont Blanc in Chambéry, France, more specifically in the LIMD (logic, computer science and discrete math) team of the LAMA (math lab).
Contact
peio.borthelle@univ-smb.fr- Github
@lapin0t- SourceHut
~lapinot- ORCID
0009-0006-7733-7439
Events
- Presented at GALOP‘24 (London, UK) “An abstract, certified account of Operational Game Semantics” (slides).
- Presented at TYPES‘23 (Valencia, Spain) a short introduction on using a spin-off of polynomial functors to describe games (slides and talk recording).
- Attended AIMXXXVI (Delft, Netherlands).
- Attended OPLSS‘22 (Eugene, Oregon, USA).
Research Interests
The main topic of my thesis (as of january 2024!) is to investigate the formalization of a particular kind of game (or trace) semantics based on automatons: operational game semantics.
I am broadly interested in programming languages (all kinds), type theory, dependently typed programming, interactive semantics (games and co). However this list is both too broad and too restrictive, so I will rather list a couple papers I recently liked (in no particular order):
- Compiling with Classical Connectives, Paul Downen and Zena M. Ariola, LMCS 2020. A very clear introduction to the mu-mu-tilde language. Pretty mind-blowing for who has been convinced that classical logic has no computational content.
- Both A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, Guillaume Allais, Robert Atkey, James Chapman, Conor McBride and James McKinna, JFP 2021 and Formal metatheory of second-order abstract syntax, Marcelo Fiore and Dmitrij Szamozvancev, POPL 2022. Both papers present the now standard approach for formalizing simply-typed languages in type theory, both in literate Agda. The first is perhaps more oriented towards the dependently-typed programmer and the second towards the category-enclined computer scientist. See also on this topic the excellent tutorial by Pierre-Evariste Dagand.
- Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus, Andreas Abel and Christian Sattler, PPDP 2019. Section 2 alone is worth the read and develops an Agda formalization of NBE for a simply typed lambda-calculus with positive connectives (here sums). Until this paper I didn’t realize that the go-to minimal example of STLC with products has only negative types. In fact quite a big (but elegant) fix is needed to deal with positives.
- The two very cute complete lattice papers Coinduction All the Way Up,
Damien Pous, LICS 2016 and Tower Induction and Up-To Techniques for CCS with
Fixed Points, Steven Schäfer and Gert Smolka, RAMICS 2017, both of which are
implemented in Damien’s Coq library
coq-coinduction. I believe they form a line of follow-ups on the two (generalized) parametrized coinduction papers by Chung-Kil Hur et al., which first introduced a similar library,paco. They introduce easily described but very powerful gadgets for dealing with exotic coinductive reasoning schemes. - Substitution, jumps, and algebraic effects, Marcelo Fiore and Sam Staton, LICS 2014. A neat development on a sort of generic effect which can be read as a high-level presentation of a low level implementation technique.
- A Linear Algebra Approach to Linear Metatheory, James Wood and Bob Atkey, TLLA 2020. A particularly compelling attempt at cracking the nut of an approachable intrinsically typed and scoped syntax for substructural calculi.
Publications
New draft paper available!
- An abstract, certified account of operational game semantics, Peio Borthelle, Tom Hirschowitz, Guilhem Jaber and Yannick Zakowski, 2024. Under submission, (draft, code, html).
- A Cellular Howe Theorem, Peio Borthelle, Tom Hirschowitz and Ambroise Lafont, LICS 2020, (pdf, doi). The writeup of work I did during my masters internship with Tom, which he continued with Ambroise (they further wrote two follow-ups, covering more instances of Howe’s method).