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.
September 2018 - present
September 2016 - August 2018
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.
University of Oxford
PhD Computer Science
2012 - 2016
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
- LNL-FPC: The Linear/Non-linear Fixpoint Calculus, with Bert Lindenhovius and Michael Mislove.
under review 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.
- 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.
To appear in ACT 2019 (Applied Category Theory). [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]
QIP 2020 (Quantim Information Processing), LICS 2018/2019(x3) (Logic in Computer Science), MFCS 2017 (Mathematical Foundations of Computer Science).
LMCS (Logical Methods in Computer Science), TCS (Theoretical Computer Science).
- 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).
A selection of talks is presented below. The complete list of my talks is available here.
Invited Talks (specialist audience)
- Recursive types for linear/non-linear quantum programming. Dagstuhl Seminar on Quantum Programming Languages. 17.09.2018. [slides]
- Baby’s First Diagrammatic Calculus for Quantum Information Processing. Logical Aspects of Quantum Information. Lorentz Center. 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, United Kingdom. 12.10.2017. [slides]
- Rewriting Families of Quantum Circuits. Logic Lounge. Simons Institute (UC Berkeley). 17.11.2016.
- Equational reasoning with context-free families of string diagrams. Invited Seminar Talk. Radboud University. 02.12.2015.
- Quantomatic – current state and case study. Celebrating 10 Years of Categorical Quantum Mechanics. Oxford, UK. 17.10.2014. [slides]
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]
Conference 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]
- 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.
- 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.