### About Me

I am a postdoctoral fellow in Computer Science at LORIA in Nancy, France. I am part of the MOCQUA team.

My research interests are in (quantum) programming languages, categorical quantum mechanics, string diagrams, automated reasoning and category theory.

My CV and links to academic profiles are at the top of the page and below you can find some information about my academic activities.

### Employment

Working on quantum programming languages.

Principal Investigator: Simon Perdrix.

Supported by the ANR/SoftQPRO and PIA-GDN/Quantex grants.

Worked on circuit description languages for quantum programming.

Principal Investigator: Michael Mislove.

Supported by the MURI grant Semantics, Formal Reasoning, and Tools For Quantum Programming.

### Education

#### University of Oxford

**PhD Computer Science**

2012 - 2016

Thesis: Rewriting Context-free Families of String Diagrams.

Supervisors: Samson Abramsky, Bob Coecke and Aleks Kissinger.

Examiners: Sam Staton (internal), Reiko Heckel (external).

#### University of Oxford

**MSc Computer Science (Distinction)**

2011 - 2012

Thesis: An Abstract Approach towards Quantum Secret Sharing.

Supervisor: Bob Coecke.

#### Jacobs University Bremen

**BSc Mathematics; BSc Computer Science**

2008 - 2011

### Papers

*Quantum Programming with Inductive Datatypes,*with Romain Péchoux, Simon Perdrix and Mathys Rennela.

**Submitted**. [pdf]*Semantics for a Lambda Calculus for String Diagrams,*with Bert Lindenhovius and Michael Mislove.

**Submitted**. [pdf]*Computational Adequacy for Substructural Lambda Calculi*.

**ACT 2020 (Applied Category Theory)**, to appear. [arxiv]*Semantics for first-order affine inductive data types via slice categories*.

**CMCS 2020 (Coalgebraic Methods in Computer Science)**, to appear. [arxiv]*LNL-FPC: The Linear/Non-linear Fixpoint Calculus,*with Bert Lindenhovius and Michael Mislove.

Accepted subject to minor revisions for the journal**LMCS (Logical Methods in Computer Science)**. [arxiv]*Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory,*with Romain Péchoux, Simon Perdrix and Mathys Rennela.

**FoSSaCS 2020 (Foundations of Software Science and Computation Structures)**. [doi | arxiv]*Mixed Linear and Non-linear Recursive Types,*with Bert Lindenhovius and Michael Mislove.

**ICFP 2019 (International Conference on Functional Programming).**[doi | arxiv]*Reflecting Algebraically Compact Functors.*

**ACT 2019 (Applied Category Theory)**, to appear. [arxiv]*Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams,*with Bert Lindenhovius and Michael Mislove.

**LICS 2018 (Logic in Computer Science).**[doi | arxiv]*A Framework for Rewriting Families of String Diagrams.*

**TERMGRAPH 2018 (Computing with Terms and Graphs).**[doi = arxiv]*Rewriting Context-free Families of String Diagrams.*

**PhD Thesis (University of Oxford, 2016).**[arxiv]*Quantomatic: A Proof Assistant for Diagrammatic Reasoning,*with Aleks Kissinger.

**CADE 2015 (Conference on Automated Deduction).**[doi | arxiv]*Equational Reasoning with Context-Free Families of String Diagrams,*with Aleks Kissinger.

**ICGT 2015 (International Conference on Graph Transformation).**[doi | arxiv]*!-Graphs with Trivial Overlap are Context-Free,*with Aleks Kissinger.

**GaM 2015 (Graphs as Models).**[doi = arxiv]*The ZX-calculus is incomplete for quantum mechanics,*with Christian Schröder de Witt.

**QPL 2014 (Quantum Physics and Logic).**[doi = arxiv]*An Abstract Approach towards Quantum Secret Sharing.*

**MSc Thesis (University of Oxford, 2012).**[pdf]*MathML-aware Article Conversion from LaTeX,*with Heinrich Stamerjohanns, Deyan Ginev, Catalin David, Dimitar Misev and Michael Kohlhase.

**DML 2009 (Towards a Digital Mathematics Library).**[published version]

### Reviewing

## Conferences:

**QIP 2020** (Quantim Information Processing), **FoSSaCS 2020** (Foundations of Software Science and Computation Structures), **LICS 2018/2019(x3)/2020(x3)** (Logic in Computer Science), **MFCS 2017** (Mathematical Foundations of Computer Science).

## Journals:

**LMCS** (Logical Methods in Computer Science), **TOPLAS** (ACM Transactions on Programming Languages and Systems), **ACS** (Applied Categorical Structures).

## Series

**Outstanding Contributions to Logic (Volume for Samson Abramsky)**.

### Research Visits

- Lorentz Center (Leiden, The Netherlands). Logic and Structure in Computer Science and Beyond (9.12.2019 - 13.12.2019).
- Schloss Dagstuhl – Leibniz Center for Informatics (Wadern, Germany). Quantum Programming Languages (16.09.2018 – 21.09.2018).
- Lorentz Center (Leiden, The Netherlands). Logical Aspects of Quantum Information (30.07.2018 - 3.08.2018).
- Simons Institute for the Theory of Computing (UC Berkeley). Logical Structures in Computation (17.11.2016 - 16.12.2016).

### Teaching

**Discrete Mathematics.**Lecturer, Tulane University. Spring 2017. [Course Website]**Categorical Quantum Mechanics.**Teaching Assistant, University of Oxford. Spring 2014, Spring 2015.**Categories, Proofs and Processes.**Teaching Assistant, University of Oxford. Fall 2014.**Quantum Computer Science.**Teaching Assistant, University of Oxford. Fall 2013, Fall 2014.**Lambda Calculus and Types.**Teaching Assistant, University of Oxford. Spring 2014.**Formal Languages and Logic.**Teaching Assistant, Jacobs University Bremen. Fall 2010.**Computability and Complexity.**Teaching Assistant, Jacobs University Bremen. Spring 2010.**Operating Systems.**Teaching Assistant, Jacobs University Bremen. Spring 2011.

### Organisation

### Talks (Selection)

A selection of talks is presented below. The complete list of my talks is available here.

## Invited Talks (international conferences)

*Inductive and Recursive Types for Quantum Programming.***Joint special session of QPL 2020 (Quantum Physics and Logic) and MFPS 2020 (Mathematical Foundations of Programming Semantics) on Quantum Programming Languages.**June 2020. [video & slides]

## Invited Talks (international seminars, special events, etc.)

*Recursive types for linear/non-linear quantum programming.***Dagstuhl Seminar on Quantum Programming Languages.**Wadern, Germany. 17.09.2018. [slides]*Baby’s First Diagrammatic Calculus for Quantum Information Processing.***Logical Aspects of Quantum Information.**Lorentz Center, Leiden, The Netherlands. 01.08.2018. [slides]*Programming String Diagrams.***Celebrating 10 years of the ZX-calculus.**University of Oxford. 10.05.2018.*Categorical models of circuit description languages.***Duskofest 2017.**Oxford, UK. 12.10.2017. [slides]*Rewriting Families of Quantum Circuits.***Logic Lounge.**Simons Institute (UC Berkeley, USA). 17.11.2016.*Quantomatic – current state and case study.***Celebrating 10 Years of Categorical Quantum Mechanics.**Oxford, UK. 17.10.2014. [slides]

## Invited Talks (group seminars)

*Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory.***Invited Seminar Talk.**LRI, Saclay, France. 07.02.2020. [slides]*Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory.***Invited Seminar Talk.**IRIF, Paris, France. 26.11.2019. [slides]*Equational reasoning with context-free families of string diagrams.***Invited Seminar Talk.**Radboud University, Nijmegen, The Netherlands. 02.12.2015.

## Invited Talks (broad audience)

*Security in a Quantum World.***NOLASEC.**New Orleans, USA. 07.11.2017. [slides]*Quantum Computing: the Good, the Bad and the (not so) Ugly.***Oriel Talks.**Oriel College (University of Oxford). 07.06.2016. [slides]*Higher-order rewriting of Quantum Circuits.***CantaBulgarian Conference.**Oxford and Cambridge Club (London, UK). 13.03.2016. [slides]

## Contributed Talks (with no formal proceedings)

*Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory.***ACT 2019.**University of Oxford. 19.07.2019. [slides]*Mixed Linear and Non-linear Recursive Types.***ACT 2019.**University of Oxford. 19.07.2019. [slides]*Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory.***CALCO 2019.**University College London. 04.06.2019. [slides]*Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams.***QPL 2018.**Halifax, Canada. 07.06.2018. [slides]*Rewriting Families of String Diagrams.***String 2017.**Oxford. 09.09.2017. [slides]*Grammar transformation with DPO rewriting.***GaM 2016.**Technische Universiteit Eindhoven. 02.04.2016. [slides]

### Software

- When I was a PhD student at Oxford, I was one of the developers of Quantomatic, which is a diagrammatic proof assistant with primary application in quantum information processing.

### Awards

- Scatcherd Scholarship for the maxium duration of 3 years (fully-funded scholarship awarded to 9 European graduate students at University of Oxford).
- MSc degree awarded with distinction for high academic performance.
- Member of the President’s List for academic achievement for all three academic years at Jacobs University Bremen.