# 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).