users:arrial:index

Victor Arrial

About me

I am now a postdoctoral researcher in the Department of Computer Science and Engineering at the University of Bologna, under the supervision of Ugo Dal Lago (University of Bologna, Bologna, Italy). We are currently trying to better understand time complexity for reversible computing in the lambda-calculus. I am also finishing my PhD on Meaningfulness in the $\lambda!$-calculus under the direction of Delia Kesner (Université Paris Cité, CNRS, IRIF, France) and Giulio Guerrieri (University of Sussex, Brighton, United Kingdom).

My research interests lie in $\lambda$-calculus$^?\!\!$, $\lambda_!$-calculus$^?\!\!$, $\lambda\mu$-calculus$^?\!\!$, explicit substitutions$^?\!\!$, reduction strategies$^?\!\!$, quantitative typing$^?\!\!$, inhabitation$^?\!\!$, Böhm$^?$ approximants and trees$^?\!\!$, Taylor expansion$^?\!\!$. I am also interested by reversible computing$^?\!$ and would like to learn more about higher order model checking$^?\!\!$.

Publications and Preprints

D. Kesner, V. Arrial and G. Guerrieri, Meaningfulness and Genericity in a Subsuming Framework (Invited paper FCSD'24, ArXiv)
V. Arrial, G. Guerrieri and D. Kesner, Genericity Through Stratification (LICS'24, ArXiv)
V. Arrial, G. Guerrieri and D. Kesner, The Benefits of Diligence (IJCAR'24, ArXiv)
V. Arrial, G. Guerrieri and D. Kesner, Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework, (POPL'23, Preprint)

See my DBLP page for a complete list.

(Credits: Delia Kesner)

Talks and Public Events

OLAS Seminar (Bologna, Italy). $\;-\;$ Genericity through Stratification (Abstract, Slides)
FCSD'24 (Tallinn, Estonia).
ITRS'24 (Tallinn, Estonia) $\;-\;$ Call-by-Value Typing Revisited, for Free ? (Abstract, Slides).
TLLA'24 (Tallinn, Estonia).
LICS'24 (Tallinn, Estonia) $\;-\;$ Genericity Through Stratification (Slides).
IJCAR'24 (Nancy, France) $\;-\;$ The Benefits of Diligence (Abstract, Slides).
Journées PPS (IRIF, Paris, France) $\;-\;$ Genericity Through Stratification (Abstract, Slides).
SMS Seminar (IRIF, Paris, France) $\;-\;$ The Benefits of Diligence (Abstract, Slides).
Non-Permanent Seminar (IRIF, Paris, France) $\;-\;$ The Bang-Calculus: An Accessible Introduction to Subsuming Paradigms (Abstract, Slides).
Chocola (ENS, Lyon, France) $\;-\;$ Genericity Through Stratification (Abstract, Slides).
DiLL (CIRM, Marseille, France) $\;–\;$ Differential $\lambda$-Calculus and Differential Linear Logic, 20 Years Later.
Séminaire LoVe (LIPN, Villetaneuse, France) $\;–\;$ Exploring the Bang-Calculus and Its Embeddings (Abstract, Slides).
GT SCALP'23 (Orléans, France) $\;–\;$ The Benefits of Diligence (Abstract, Slides).
HOR'23 (Sapienza, Rome, Italy) $\;-\;$ A Deeper Study of $\lambda!$-Calculus Simulations (Abstract, Slides).
FSCD'23 (Sapienza, Rome, Italy).
AB60 (IRIF, Paris, France) Workshop in Honour of Antonio Bucciarelli's 60th Birthday $\;–\;$ Quantitative Inhabitation with Delia Kesner (Slides).
Journées PPS (IRIF, Paris, France) $\;-\;$ 24-25 Mai 2023.
CHoCoLa (ENS, Lyon, France) $\;-\;$ Rencontre du 5 Mai 2023.
Séminaire Logique et Interactions (I2M, Marseille, France) $\;-\;$ The Bang-Calculus, Inhabitation and Approximants (Abstract, Slides Partie 1, Slides Partie 2).
FoPSS'23 (Ceub, Bertinoro, Italy) Winter School $\;-\;$ Quantitative Aspects of Program Semantics, Verification and Transformation.
POPL'23 (Boston, USA) $\;-\;$ Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework (Paper, Artifact, Slides, Video).
Non-Permanent Seminar (IRIF, Paris, France) $\;–\;$ Introduction to Lambda-Calculus and Quantitative Typing Systems (Blackboard).
TE60 (CNAM, Paris, France) Workshop in Honour of Thomas Ehrhard's 60th Birthday.
TYPES'22 (LS2N, Nantes, France) $\;–\;$ Quantitative Inhabitation in Call-by-Value (Abstract, Video).
NIETS'22 (CS Dep., Bath, UK) $\;–\;$ Quantitative Inhabitation in Call-by-Push-Value (Abstract).
SINFIN'22 (IRIF, Paris, France) $\;–\;$ Quantitative Inhabitation through Call-by-Push-Value (Slides).
GT SCALP'21 (UPEC, Fontainebleau, France) $\;–\;$ Inhabitation in Call-by-Push-Value (Slides).

Teaching

2024-2025 :
- B5026 M1 - Introduction to Computability and Complexity (TD).
2023-2024 :
- LMFI M2 : Proofs and Programs (Guest Lecturer).
- IP1 : Introduction à la Programmation Java (CM + TD + TP).
- Poo-IG : Programmation Orientée Objet - Interface Graphique (TP + Projet).
- CProj : Conduite de Projet (TP).
2022-2023 :
- IP1 : Introduction à la Programmation Java (CM + TD + TP).
- PF1 : Principes de Fonctionnement des Machines Binaires (TD + TP).
2021-2022 :
- IP2 : Initiation à la Programmation Java (TD + TP).
- CI2 : Concepts Informatiques (TD).

Past projects

M2 $\;–\;$ Inhabitation in Call-by-Push-Value, $\;$ under directions of Delia Kesner et Giulio Guerrieri at IRIF.
M1 $\;–\;$ Inhabitation in the $\lambda\mu$-Calculus, $\;$ under directions of Delia Kesner at IRIF.
$\,$L3 $\;–\;$ Curry-Howard Correspondence and Linear Logic, $\;$ under directions of Jules Chouquet and Léo Stefanesco at IRIF.
$\,$L2 $\;-\;$ Regression and Classification Problems for Machine Learning, $\;$ under directions of Pierre Latouche at SAMM.

Miscellaneous

Here is my curriculum vitae (last update on 06/06/2024)

A few friends doing wonderful work:
Klara Nosan, Roman Kniazev, Lucie Guillou, Alexandre Moine, Martin Pépin, Loïc Peyrot, Vincent Moreau, Clément Ducros, Adrienne Lancelot …

Contact

*Mail :*	$(\lambda x. \; \text{arrial} \: x \; \text{irif}.\text{fr})\;@$
*Office :*	$3018$