Samuel Arsac

Doctorant en informatique à l'ENS Lyon

Mon CV.

Le dépôt de mon travail actuel sur la formalisation en Rocq de théorie des catégories pour la réécriture de graphes est ici.

J'ai fait un tutoriel pour le Groupe de travail sur les assistants de preuve à l'ENS Lyon le 23 mars 2026. Les fichiers sont ici, avec les autres tutoriels.

Publications

Formalizing adhesive category theory in Rocq (JFLA 2025)

Adhesive Category Theory for Graph Rewriting in Rocq (CPP 2026)

Stages

2022-2023: Université Nationale de Séoul, Software Fundations Lab, supervisé par Chung-Kil Hur

Intitulé: Adapting Conditional Context Refinement to real world programs.

2022 : ENS Lyon, LIP, équipe PLUME, supervisé par Russ Harmer & Damien Pous

Intitulé : Coq formalization of the concurrency theorem in graph transformation via diagrammatic reasoning in quasi-topoi.
Le rapport (en anglais) et le dépot git associé.

2021 : université de Strathclyde, Glasgow, supervisé par Robert Atkey

Intitulé : Expressivity of BCI algebras.
Le rapport (en anglais) et le dépot git associé.
Note : ce rapport contient des erreurs en ce qui concerne la réversibilité, et l'implémentation en Coq n'est pas parfaite.

2020 : ENS Lyon, LIP, équipe MC2, supervisé par Omar Fawzi

Intitulé : Multiple access channels with non-signaling resources.
Le rapport

Projets

Activité d'informatique débranchée sur les chemins eulériens, destinée aux lycéens.

La fiche d'activité

Travail d'Initiative Personnelle Encadré (TIPE)

Réalisé en 2018 - 2019, en deuxième année de CPGE.
Le rapport