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" }
|
|
]
|
|
```
|
|
|