About Me
I am a researcher at Inria. I am part of the QuaCS team located at LMF in Île-de-France.
My research interests are in quantum and probabilistic programming languages, categorical quantum mechanics, string diagrams and category theory.
I am originally from Sofia, Bulgaria, where I was born and raised. I can speak English (fluent), Bulgarian (native) and a bit of French.
Employment
Researcher in the QuaCS team. Previously, I was a member of the MOCQUA team at Inria/LORIA.
Quantum programming languages.
Principal Investigator: Simon Perdrix.
Supported by the ANR/SoftQPRO and PIA-GDN/Quantex grants.
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
Prior to that, I studied at the Sofia High School of Mathematics in Sofia, Bulgaria.
Papers
- Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages, with Titouan Carette and Louis Lemonnier.
LICS 2023 (Logic in Computer Science). [doi | arxiv] - Type-safe Quantum Programming in Idris, with Liliane-Joy Dandy and Emmanuel Jeandel.
ESOP 2023 (European Symposium on Programming). [arxiv | doi | software] - Quantum Expectation Transformers for Cost Analysis, with Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix.
LICS 2022 (Logic in Computer Science). [doi | arxiv] - Semantics for Variational Quantum Programming, with Xiaodong Jia, Andre Kornell, Bert Lindenhovius and Michael Mislove.
POPL 2022 (Principles of Programming Languages). [doi | arxiv] - Commutative Monads for Probabilistic Programming Languages, with Xiaodong Jia, Bert Lindenhovius and Michael Mislove.
Preprint. Extended version of our LICS 2021 paper. [pdf] - The Central Valuations Monad, with Xiaodong Jia and Michael Mislove.
CALCO 2021 (Conference on Algebra and Coalgebra in Computer Science ). Early Ideas Track. [doi | arxiv ] - Commutative Monads for Probabilistic Programming Languages, with Xiaodong Jia, Bert Lindenhovius and Michael Mislove.
LICS 2021 (Logic in Computer Science). [doi | arxiv] - Quantum Programming with Inductive Datatypes, with Romain Péchoux, Simon Perdrix and Mathys Rennela.
Submitted. Extended version of our FoSSaCS 2020 paper. [pdf] - Semantics for a Lambda Calculus for String Diagrams, with Bert Lindenhovius and Michael Mislove.
Samson Abramsky on Logic and Structure in Computer Science and Beyond. [doi] - Computational Adequacy for Substructural Lambda Calculi.
ACT 2020 (Applied Category Theory). [doi = arxiv] - Semantics for first-order affine inductive data types via slice categories.
CMCS 2020 (Coalgebraic Methods in Computer Science). [doi | arxiv] - LNL-FPC: The Linear/Non-linear Fixpoint Calculus, with Bert Lindenhovius and Michael Mislove.
LMCS (Logical Methods in Computer Science). [doi | 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). [doi = 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]
Special Interest Groups
- Member of the IFIP TC1/TC2 Working Group on Foundations of Quantum Computation.
Program Committees
- QPL 2023. PC co-chair for the international conference on Quantum Physics and Logic in 2023.
- ACT 2023. PC member for the international conference on Applied Category Theory in 2023.
- QPL 2022. PC member for the international conference on Quantum Physics and Logic in 2022.
- ACT 2022. PC member for the international conference on Applied Category Theory in 2022.
- PlanQC 2022. PC member for the international workshop on Programming Languages for Quantum Computing in 2022.
- WADT 2022. PC member for the international Workshop on Algebraic Development Techniques in 2022.
- ACT 2021. PC member for the international conference on Applied Category Theory in 2021.
- QPL 2021. PC member for the international conference on Quantum Physics and Logic in 2021.
- PlanQC 2021. PC member for the international workshop on Programming Languages for Quantum Computing in 2021.
Organisation
Supervision
- Kinnari Dave. PhD student (current).
- Louis Lemmonier. PhD student (current).
- Hugo Massonnat. Research internship on quantum programming (March – July 2022).
- Liliane-Joy Dandy. Research internship on quantum programming (March – July 2021). “Research Internship Prize” at École Polytechnique. Paper: Qimaera: Type-safe (Variational) Quantum Programming in Idris, with Liliane-Joy Dandy and Emmanuel Jeandel. Preprint. [pdf | software]
Research Visits
- Lorentz Center (Leiden, The Netherlands). New challenges in programming language semantics (28.11.2022 - 2.12.2022).
- 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).
Reviewing
Conferences:
CSL 2021 (Computer Science Logic), QIP 2020 (Quantim Information Processing), FoSSaCS 2020 (Foundations of Software Science and Computation Structures), LICS 2018/2019(x3)/2020(x3)/2021 (Logic in Computer Science), MFCS 2017/2021 (Mathematical Foundations of Computer Science), ESOP 2022 (European Symposium on Programming).
Journals:
LMCS (Logical Methods in Computer Science), TOPLAS (ACM Transactions on Programming Languages and Systems), ACS (Applied Categorical Structures), TQC (ACM Transactions on Quantum Computing), Quantum.
Series
Outstanding Contributions to Logic (Volume for Samson Abramsky).
Software
- Qimaera: Idris libraries for type safe (variational) quantum programming.
- When I was a PhD student at Oxford, I was one of the developers of Quantomatic.
Teaching
- Quantum Computing. Lecturer, Université de Lorraine. Winter 2021, Winter 2022.
- Programming in Haskell. Lecturer, Université de Lorraine. Winter 2021.
- 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.
- Operating Systems. Teaching Assistant, Jacobs University Bremen. Spring 2011.
- Formal Languages and Logic. Teaching Assistant, Jacobs University Bremen. Fall 2010.
- Computability and Complexity. Teaching Assistant, Jacobs University Bremen. Spring 2010.
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.)
- Semantics for Variational Quantum Programming. Logic, Quantum Computing, and Artificial Intelligence. Virtual. 03.07.2021.
- 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)
- Semantics for first-order affine inductive data types via slice categories. Invited Seminar Talk. Concurrent Games Cafe. [slides]
- 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)
- Commutative Monads for Probability in Domain Theory. Logic of Probabilistic Programming. CIRM, Marseille, France, 04.02.2022. [website]
- 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]
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.