140 lines
5.3 KiB
Markdown
140 lines
5.3 KiB
Markdown
---
|
||
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" }
|
||
]
|
||
```
|
||
|