---
title: My homepage
author: Samy Avrillon
shortbio: Wishes the world was self-compatible
description-meta: Short bio for meta-data
og-url: https://mysaa.bernard.com.de/
location: Office GN1.326N, ENS de Lyon, 46 allée d'Italie, 69007 Lyon, France
email: samy.avrillon@ens-lyon.org
clickable-email: true
picture: img/myself3.jpg
picture-round: true
side-by-side: true
disable-dark-mode: false
pronouns: They/them
og-picture: https://basicpage.github.io/img/profile.png
orcid: 0009-0003-3476-0366
dblp: https://dblp.org/pid/427/9353.html
#hal: https://hal.science/
#mastodon: https://lipn.info
discord: mysaajava
github: MysaaJava
git: https://git.bernard.com.de
footer: >-
  Based on this nice
  [basicpage template](https://github.com/basicpage/basicpage.github.io)
  thanks for their work
---

Since high school studied how text could be transformed into programs, proofs or anything that makes sense.
Trying to make the world self-compatible.

I am currently doing my PhD thesis with Cyril Cohen in [ENS de Lyon](https://www.openstreetmap.org/way/95144113).
My work subject is [Trocq](https://github.com/rocq-community/trocq), a Rocq library doing proof transfer.
You can find most of my notes and presentation I made about this on [my Inria gitlab](https://gitlab.inria.fr/savrillo/phd-redactions).

# Curriculum

## Schools
  
### 2018-2021: High-school preparatory classes (CPGE)
[Lycée Lafayette](https://www.openstreetmap.org/way/44170361) & [Lycée Blaise Pascal](https://www.openstreetmap.org/way/144713008)
Preparatory classes for the ENS competitive exam, extended to three years

### 2021-2025: ENS diploma curriculum
[ENS de Lyon](https://www.openstreetmap.org/way/95144113)
Licence degree in 2022, first year of master's degree in 2023.
Register as "external studies" for the second year of the Master's degree.
Fourth year of internships.

### 2023-2024: MPRI (Master Parisien de la Recherche en Informatique)
[Université Paris Cité](https://www.openstreetmap.org/way/286296494)
Second year of master degree outside of the ENS because of a course selection that fit my interests a lot more.


## Internships

### Summer 2022: Program Equivalences in (Featherweight) Java
8 week internship with Daniele Varacca & Clément Aubert in [LACL, Créteil, France](https://www.openstreetmap.org/way/37022786)
I did create an interesting notion of context and equivalence in this minimal object-oriented language.

### Summer 2023: Logic as a Second-Order Generalized Algebraic Theory
3 month internship with Kaposi Ambrus & Thorsten Altenkirsch at [ELTE, Budapest, Hungary](https://www.openstreetmap.org/way/1318152907)
I did implement a formalization of Propositional and First order Logic in Agda, based upon a SOGAT definition of those logics.

### Summer 2024: Categorical semantics of the reduction of GATs to two-sorted GATs
4.5 month internship with Ambroise Lafont at [LIX, Palaiseau, France](https://www.openstreetmap.org/way/548438043)
I did prove a known GAT tranformation to be correct and to preserve some properties. 
This work lead to a publication in 2026 that you can find here: https://arxiv.org/abs/2601.19426

### Winter 2024/2025: Formalizing modal logic with hyperdoctrines
5 month internship with Kenji Maillard at [LMU, München, Deutschland](https://www.openstreetmap.org/way/376680733)
I studied Hyperdoctrines and implemented them in the Proof Assistant Lean, along with an extension to any modal logic, taking guarded logic as an example.

### Spring 2025: Getting the hang of Trocq
3.5 month internship with Cyril Cohen at [LIP, Lyon, France](https://www.openstreetmap.org/way/95144113)
Applications and extensions of Trocq for formalized mathematics in proof assistants based on CIC



# Publications

## Journal papers

``` json {.paper}
"title": "For Generalised Algebraic Theories, Two Sorts Are Enough",
"authors": "Samy Avrillon, Ambrus Kaposi, Ambroise Lafont, Niyousha Najmaei, Johann Rosain",
"year": "2026",
"url": "https://arxiv.org/abs/2601.19426",
"files": [
  { "text": "Paper", "type": "pdf", "src": "files/2026-GATsTwoSorts.pdf" }
]
```


## Internship reports

``` json {.paper}
"title": "Modal Hyperdoctrines",
"authors": "Samy Avrillon",
"year": "2025",
"url": "https://github.com/MysaaJava/guarded-lean/tree/plr",
"files": [
  { "text": "Presentation", "type": "pdf", "src": "files/2025-M2-presentation.pdf" }
]
```

``` json {.paper}
"title": "2-sortification",
"authors": "Samy Avrillon",
"year": "2024",
"url": "https://git.bernard.com.de/Mysaa/M2Internship",
"files": [
  { "text": "Report", "type": "pdf", "src": "files/2024-M2-Report.pdf" },
  { "text": "Presentation", "type": "pdf", "src": "files/2024-M2-Presentation.pdf" }
]
```

``` json {.paper}
"title": "Logic as a Second-Order Generalized Algebraic Theory",
"authors": "Samy Avrillon",
"year": "2023",
"url": "https://github.com/MysaaJava/m1-internship",
"files": [
  { "text": "Report", "type": "pdf", "src": "files/2023-M1-Report.pdf" },
  { "text": "Presentation", "type": "pdf", "src": "files/2023-M1-Presentation.pdf" }
]
```

``` json {.paper}
"title": "Featherweight Java",
"authors": "Samy Avrillon",
"year": "2022",
"url": "https://gitlab.aliens-lyon.fr/savrillo/stage-2022",
"files": [
  { "text": "Report", "type": "pdf", "src": "files/2022-L3-Report.pdf" },
  { "text": "Presentation", "type": "pdf", "src": "files/2022-L3-Presentation.pdf" }
]
```