Computer Laboratory

Jamie Vicary

Professor of Future Computation

Royal Society University Research Fellow

Fellow of King's College

Email: jamie.vicary@cl.cam.ac.uk

Office: FS22

Telephone: 01223 7(63510)

Address: Computer Laboratory, University of Cambridge,
J. J. Thomson Avenue, Cambridge, CB3 0FD, UK

Graduate textbook on category theory and quantum computation now available!

• OUP
• Amazon.co.uk
• Amazon.com

My research aims to develop new logical and structural techniques, with the goal to transform the way we compute in the future, across a range of areas including quantum and classical computation. A lot of my research uses the tools of category theory, a rich abstract language for understanding how interacting systems process information. I am also interested in studying category theory itself, finding ways to make it more powerful and easier to use. I work as part of the Cambridge Logical Structures Hub (CLASH) research group in the department.

I love welcoming new members to my team. If you are interested in working with me as an undergraduate, Masters or PhD student, or if you'd like to ask about postdoctoral research opportunities, send me a message and I'd be happy to chat.

• Geometrical higher category theory. A longstanding problem in higher category theory has been to define a semistrict theory, where part of the syntax is trivialized, making the theory easier to use. One standard approach to this is string diagrams, and this has been a major focus over the last several years, resulting in the graphical proof assistant homotopy.io for semistrict n-categories (LICS2022#P41, LICS2019#P36, LICS2017#P29.) The latest version is developed in Rust (github), and allows construction of composites and homotopies in arbitrary dimension, in a strictly associative and unital setting, with advanced visualisation options including Morse projection, 3d and 4d rendering, and LaTeX export. Collaborators include Krzysztof Bar, Nathan Corbyn, Lukas Heidemann, Nick Hu, David Reutter and Calin Tataru.
• Type theory for higher category theory. An exciting major line of current activity is using type theory to understand the properties of higher categories. In recent work we gave a new definition of strictly unital ∞-category (LICS2022#P36) which has better properties than the one previously in the literature, and also the first general definition of strictly associative ∞-category (2109.01513#P39). Collaboration with Eric Finster, David Reutter and Alex Rice.
• Complexity of geometrical calculi. We have a developing interest in complexity-theoretic aspects of geometrical techniques, an exciting area where much remains to be done. We have shown that the word problem for monoidal categories can be solved in quadratic time (LMCS2018#P34), and that the word problem for braided monoidal categories is at least as hard as the unknot problem (ACT2021#P40). Joint work with my student Antonin Delpeuch.
• Quantum combinatorics. Our goal in this area is to understand the nature of a wide range of quantum combinatorial objects, and how they interact with each other, using the tools of category theory. Major contributions here include the definition of quantum Latin squares (QIC2015#P17, QIP 2016), and a new way to use higher category theory to define unitary error bases, quantum Latin squares and other combinatorial objects as biunitary vertices in the 2-category of 2-Hilbert spaces (LICS2012#P8, QIP 2017). Joint work with my students Benjamin Musto and David Reutter.
• Dynamics of quantum systems. Categorical techniques have powerful application in the area of quantum dynamics, where we can use simple geometrical rules to understand the origins of computational effects. In a new collaboration, we recently used these techniques to show that exact measurement correlations can be computed in heterogenous qubit networks even when measurements are interspersed arbitrarily with unitary gates (2207.00025#P42). In other work we showed how a shaded tangle calculus gives a powerful language for understanding a wide range of quantum computational phenomena, including quantum error correction, where we can see for the first time the errors being "captured" by "bubbles" and eliminated (PRSA#P30). We also showed how string diagrams can be used to understand the dynamics of some important quantum algorithms (LICS2013#P9). Collaborators include Pieter Claeys, Marius Henry, Austen Lamacraft and David Reutter.
• Topological quantum field theory. If a quantum field theory has the property that its partition function depends only on the diffeomorphism class of the manifold, it is called topological. We showed that 3-dimensional TQFTs extended to points are classified precisely by modular tensor categories equipped with certain extra data, settling an important long-standing conjecture (1509.06811#P18). Other work on 2-dimensional TQFT showed that the wormhole creation process is identical to the entanglement creation process, verifying in a topological setting the ER=EPR hypothesis of Maldacena and Susskind (CQG2014#P12). Collaborators include John Baez, Bruce Bartlett, Christopher Douglas and Christopher Schommer-Pries.

Biography. I joined Cambridge as a member of faculty in 2020. Before that I was a faculty member in the Theoretical Computer Science research group in Birmingham, which followed several years as a postdoctoral researcher in the Quantum Group in the Computer Science department at Oxford, and also at the Centre for Quantum Technologies in Singapore. I did my PhD in Physics at Imperial College London under the supervision of Professor Chris Isham, which was awarded in 2009, and which focused on the mathematical foundations of quantum computation. Before that I took the fantastic Maths Part III course in Cambridge with a specialization in quantum physics, which followed a first degree in Physics at Mansfield College in Oxford.

I am always interested in taking on new PhD or Masters students, or starting new collaborations. If you're interested in my research, feel free to get in touch.

The future

• November 2023. Zhanghan Wang is one of the organizers of a workshop Topology, Quantum Error Correction and Quantum Gravity at UCLA, where I will be an invited speaker.
• June 2023. I will be an invited speaker at LOOPS '23 at the Mathematical Research and Conferences Centre in Bedlewo, Poland.

The past

• May 2023. New preprint "Posetal diagrams for logically-structured semistrict higher categories", which defines a new type of string diagram powerful enough to represent categorical limits. (With Chiara Sarti.)
• May 2023. New preprint "A layout algorithm for higher-dimensional string diagrams" which uses factorization systems in the category of posets to extract the constraint data necessary for computing attractive layouts of higher-dimensional string diagrams. (With Calin Tataru.)
• April 2023. I have started a secondment in the Department for Science, Innovation and Technology, where I will be working for two days per week for the rest of the year. I am enjoying the exciting challenge of applying my scientific training in the government world!
• April 2023. I will be speaking at the Midlands Graduate School 2023, delivering an invited lecture course on "Computational models of higher categories".
• February 2023. New preprint "A 2-categorical model for exactly-solvable many-body quantum dynamics" (with Pieter Claeys and Austen Lamacraft) which uses 2-categorical technology to unify Prosen's "round-a-face" dual unitarity with traditional dual unitarity, and shows how these are distinct "quantum phases" which can interact richly.
• February 2023. New preprint "Strictly associative and unital ∞-categories as a generalized algebraic theory" (with Eric Finster and Alex Rice). Here we give the first definition of strictly associative and unital ∞-category, along with a computer implementation.
• December 2022. The Tenth Symposium on Compositional Structures (SYCO 10) will be hosted by Chris Heunen in Edinburgh on 19-20 December.
• October 2022. Welcome to Chiara Sarti and Haiqi Wu who have started with me as PhD students.
• September 2022. The Ninth Symposium on Compositional Structures (SYCO 9) will take place on 8-9 September at the University of Insubria, organized by Nicoletta Sabadini and Elena di Lavore.
• August 2022. Preprint "Computads for weak ∞-categories as an inductive type" (with Christopher Dean, Eric Finster, Ioannis Markakis and David Reutter) where we give a new elementary, inductive definition of computad, and show how to derive many important properties of computads from first principles.
• August 2022. Welcome to Manuel Araujo who will be starting in my group as a postdoc.
• July 2022. Preprint "Exact dynamics in dual-unitary quantum circuits with projective measurements" (with Pieter Claeys, Marius Henry and Austen Lamacraft), which shows how we can get exactly solvable correlations in heterogenous lattices which combine biunitary dynamics with measurements in a unitary basis. UPDATE: Accepted for publication in Physical Review Research.
• June 2022. I have been awarded the Birkhoff–von Neumann Prize 2022 for my research on quantum foundations.
• May 2022. Two papers accepted to LICS 2022, "Zigzag normalisation for associative n-categories" and "A type theory for strictly unital ∞-categories".
• May 2022. If you're an undergraduate student in Cambridge and love programming in Rust, you're welcome to apply for my summer project working on our homotopy.io proof assistant.
• May 2022. Preprint "Zigzag normalisation for associative n-categories" (with Lukas Heidemann and David Reutter), which gives a recursive algorithm for normalizing geometrical composites, and forms a key part of our proof assistant homotopy.io. UPDATE: Accepted to LICS 2022.
• January 2022. Quanta article "Euler's 243-Year Old 'Impossible' Puzzle Gets a Quantum Solution" discusses my research on quantum Latin squares.
• September 2021. Preprint "A type theory for strictly associative ∞-categories" (with Eric Finster and Alex Rice), which extends our previous strictly-unital work to include the case of strict associators.
• September 2021. Preprint "Traced monoidal categories as higher structures in Prof" (with Nick Hu), which gives a new way of working with traced monoidal categories via string diagrams in a monoidal bicategory. UPDATE: accepted for MFPS 2021.
• May 2021. Preprint "The word problem for braided monoidal categories is unknot-hard" (with Antonin Delpeuch), which shows that deciding equality of morphisms in a free monoidal category is at least as hard as determining if a link is unknotted. UPDATE: accepted for ACT 2021.
• December 2020. I will be giving a talk in the Homotopy Type Theory Electronic Seminar Talks series.
• November 2020. I will be giving a talk in Andrej Bauer's Every Proof Assistant seminar series.
• November 2020. I will be giving the Mathematics Colloquium at Dalhousie University.
• October 2020. Welcome to Ioannis Markakis who has started a PhD with me at the University of Cambridge.
• July 2020. Preprint "A type theory for strictly-unital ∞-categories" (with Eric Finster and David Reutter), which gives a new type-theoretical definition of strictly unital ∞-categories. UPDATE: now accepted to LICS 2022.
• April 2020. The first Online Worldwide Seminar on Logic and Semantics (OWLS) was a huge success, with 359 participants at its peak, and hundreds of people taking advantage of the virtual coffee breaks to socialize. See you all 2 weeks time!
• April 2020. I have moved to join the Computer Laboratory at the University of Cambridge, working in the in the Theory, Programming and Semantics group.
• March 2020. With Alexandra Silva and Pawel Sobocinski, I am delighted to announce the Online Worldwide Seminar on Logic and Semantics (OWLS), a new online-only international seminar series, with "coffee breaks" before and after each seminar giving a nontrivial social component. Join our first seminar at 2pm UTC+1 on Wednesday April 1.
• December 2019. I will be attending the Sixth Symposium on Compositional Structures (SYCO 6) in Leicester on 16-17 December.
• November 2019. My textbook "Categories for Quantum Theory: An Introduction", coauthored with Chris Heunen, has been published by Oxford University Press!
• November 2019. I will be giving an invited talk at an LMS Meeting on Category Theory and its Applications, organized by Andrew Smith and Peter Guthmann at the University of Leicester.
• October 2019. Welcome to Alex Rice and Calin Tataru who have started a PhD with me in Birmingham, and Lukas Heidemann and Nick Hu who have started a PhD with me in Oxford.
• September 2019. I will be co-organizing SYCO 5 and STRINGS 3, which will be held together in Birmingham on 4-6 September.
• August 2019. I have been invited to serve on the programme committee for QPL 2020.
• August 2019. My student David Reutter has successfully defended his DPhil thesis. Congratulations David!
• August 2019. Noah Snyder from the University of Indiana will be visiting.
• August 2019. The paper "Quantum teleportation with infinite reference frame uncertainty and without prior alignment" (with Dominic Verdon) has been accepted by Physical Review A.
• June 2019. I attended LICS 2019, and with David Reutter gave a presentation of our paper "High level methods for homotopy construction in associative n-categories".
• June 2019. Invited tutorial "Higher Categories and Quantum Structures" as part of Quantum Symmetries 2019 at Ohio State University, organized by David Penneys.
• April 2019. I will be giving a mini course at the 2019 Midland Graduate School on the Foundations of Computing Science with the title "Monoidal Categories and Higher Categories".
• March 2019. The paper "High-level methods for homotopy construction in associative n-categories" (with David Reutter) has been accepted for presentation at LICS 2019.
• March 2019. The Third Symposium on Compositional Structures (SYCO 3) took place on March 27 and 28 in the Department of Computer Science in Oxford, with 70 participants and 30 submissions.
• March 2019. I presented the contributed talk "Introducing homotopy.io" at SYCO 3, giving an overview of the new tool developed with Lukas Heidemann and Nick Hu.
• March 2019. I co-presented a live video podcast from the 4th Quantum Computing Hackathon, taking place at the Said Business School in Oxford.
• March 2019. My student David Reutter has been awarded a postdoctoral position with Peter Teichner at the Max Planck Institute for Mathematics in Bonn, to start in September 2019. Congratulations David!
• February 2019. New preprint "High-level methods for homotopy construction in associative n-categories" (with David Reutter), giving a general contraction principle for proof construction in homotopy.io.
• February 2019. My student Dominic Verdon, currently a postdoc with Ashley Montanaro in Bristol, has successfully defended his doctoral thesis "Algebraic quantum structures for reference frame–independent quantum teleportation and pseudotelepathy". Congratulations Dominic!
• January 2019. I have been invited to serve on the programme committees for ACT 2019 and QPL 2019.
• January 2019. I have been invited to join the Royal Society's International Exchanges panel.
• December 2018. Paper "Biunitary constructions in quantum information" (with David Reutter) accepted to Higher Structures.
• December 2018. I gave an invited talk at the 2018 Midland Graduate School Christmas Seminar.
• December 2018. SYCO 2 took place on December 17-18 at the University of Strathclyde, UK, organized by Fredrik Forsberg.
• November 2018. I will be giving a seminar to the Theoretical Physics group in Birmingham about the classification of 3d topological quantum field theories.
• October 2018. I have been elected to serve on the FSCD Steering Committee as Workshop Chair.
• September 2018. Research visit from Lucy Zhang, University of Toronto, to my group in Oxford.
• September 2018. I will be talking about category theory and visual proofs at RCon3, a cryptocurrency conference in Berlin.
• August 2018. We received 42 submissions for the First Symposium on Compositional Structures (SYCO 1), an exciting new meeting aiming to bring together the diverse communities whose work focuses on the theory and application of category-theoretical tools.
• August 2018. I have been invited to be a founding editor of the new journal Compositionality.
• July 2018. Invited keynote talk at the 13th International Workshop on User Interfaces for Theorem Provers, Oxford, UK.
• July 2018. Invited keynote talk at Young Researchers in Mathematics, University of Southampton, UK.
• June 2018. Paper "Coherence for Frobenius pseudomonoids and the geometry of linear proofs" (with Lawrence Dunn) accepted for publication in Logical Methods in Computer Science.
• June 2018. Paper "Tight reference frame–independent quantum teleportation" (with Dominic Verdon) accepted to Physical Review A.
• June 2018. Attending QPL 2018 in Halifax, a great conference in a wonderful city, and giving on a talk on our paper "Orthogonality for quantum Latin isometry squares" (joint work with Benjamin Musto).
• June 2018. David Reutter and I had a great time at the Hay Festival, where we gave two sessions of our workshop "Build Your Own Quantum Computer!".
• May 2018. My student Vaia Patta has successfully defended her doctoral thesis, entitled "Category Theory for Statistical Mechanics". Congratulations Vaia!
• May 2018. My student Dominic Verdon has been offered a postdoctoral position in Ashley Montanaro's quantum information group at Bristol, to work on quantum algorithms and communication protocols. Congratulations Dominic!
• April 2018. New preprint "Normal forms for planar connected string diagrans" (with Antonin Delpeuch), giving an algorithm to determine isotopy of planar connected diagrams in O(nm) time, where n is the number of vertices and m is the number of edges.
• April 2018. New preprint "Orthogonality for quantum Latin isometry squares" (with Benjamin Musto), describing a generalization of the orthogonality property of quantum Latin squares, with applications to perfect tensors and unitary error bases. UPDATE: accepted for QPL 2018.
• April 2018. For most of this month I will be visiting Christine Tasson and Jean Krivine at IRIF, Paris, France.
• February 2018. New preprint "Quantum teleportation with infinite reference frame uncertainty" (with Dominic Verdon), describing new a way to increase the fidelity of quantum teleportation without any additional resource overhead, and without a prior synchronization step.
• February 2018. Invited talk at Higher Gauge Theory and Quantum Matter, University of Leeds, UK.
• January 2018. I have been interviewed by News.com.au for an article on quantum computing.
• January 2018. I have joined the Theory Group of the School of Computer Science at the University of Birmingham as a Senior Lecturer and Royal Society University Research Fellow, to be held jointly with my position as Senior Research Fellow in Oxford.
• November 2017. I have been interviewed by BBC TV about quantum computers for their technology program "Click!" (my bits start at about 2:20, 3:20 and 5:25.)
• October 2017. Welcome to Jean-Simon Lemay, who has started a PhD with me at the University of Oxford.
• October 2017. I have been interviewed by BBC News for the article "How do you build the next-generation quantum internet?".
• September 2017. I am serving as Workshop Chair for FSCD 2017, where we will be hosting 11 fantastic workshops: EUTypes, HDRA, HoTT, IFIP, IWC, LFMTP, SD, String, TLLA, UNIF and WPTE.
• August 2017. I have been offered a Royal Society University Research Fellowship.
• June 2017. I gave workshops at the Hay Festival and Cheltenham Science Festival (with David Reutter) where members of the public could build their own quantum computer.
• May 2017. Papers "A classical groupoid model for quantum networks" and "Biunitary structures for quantum information" (with David Reutter) accepted for CALCO 2017.
• April 2017. Group seminar at IRIF, Paris, France.
• March 2017. Extended abstract for "Data structures for quasistrict higher categories" (with Krzysztof Bar) accepted for LICS 2017.
• February 2017. I have been offered an EPSRC Early Career Fellowship.
• January 2017. New preprint "A classical groupoid model for quantum networks" (with David Reutter), describing new bicategorical structures for classical networking, which can emulate nontrivial quantum protocols, including quantum key distribution.
• January 2017. New preprint "Shaded tangles for the design and verification of quantum programs" (with David Reutter), describing new techniques for drawing quantum circuits as shaded tangles, so that circuit verification is just knot isotopy. We also give a new state transfer algorithm for a cluster-based quantum computer, give new constructions of error correcting codes based on unitary error bases, and identify surprising topological properties of the quarter-turn about the X-axis on the Bloch sphere.
• December 2016. Our proof assistant Globular has been loaded 10,000 times by 2,500 users!
• November 2016. Research visit from Jean Krivine, IRIF, Paris.
• November 2016. Paper on biunitary constructions (with David Reutter) accepted to QIP 2017, the top international quantum computing conference.
• October 2016. New 112-page preprint "Data structures for quasistrict higher categories" (with Krzysztof Bar) gives the theoretical foundations for our proof assistant Globular, including a new definition of semistrict 4-category.
• September 2016. New preprint "Biunitary constructions in quantum information" (with David Reutter.) Many new construction methods relating Hadamard matrices, unitary error bases, quantum Latin squares and controlled families, all illustrated with the graphical calculus for 2-categories.
• August 2016. Public lecture "Our quantum future" at the University of Dalhousie, Halifax, Canada, introducing quantum computers and discussing the possible impact they might have on society.
• July 2016. Invited lecturer for the AARMS Summer School, University of Dalhousie, Halifax, Canada. I gave a 30-hour course on Categories, Quantum Computation and Topology to 30 excellent and motivated students, including a big practical component using Globular.
• June 2016. The paper "The categorified Heisenberg algebra I: a combinatorial representation" (with Jeffrey Morton), describing a combinatorial interpretation of Khovanov's categorification of the Heisenberg algebra, accepted to appear in JPAA.
• May 2016. New result (with Krzysztof Bar), formalized here: every adjunction in a semistrict 4-category can be promoted to satisfy the butterfly equations.
• April 2016. Paper "Globular: a proof assistant for higher rewriting" (with Krzysztof Bar and Aleks Kissinger) accepted for FSCD 2016.
• March 2016. Preprint "Tight reference frame–independent quantum teleportation" (with Dominic Verdon) available online, describing the first zero-overhead procedure for quantum teleportation without a shared reference frame. UPDATE: accepted for conference QPL 2016. UPDATE: accepted for PRA.
• March 2016. Semistrict 4-categories are now supported by the proof assistant Globular.
• January 2016. Preprint "Surface proofs for linear logic" (with Lawrence Dunn) available online, describing a coherence result for Frobenius pseudomonoids and swallowtailators, with applications to proof equivalence for linear logic. UPDATE: different parts of this work accepted for workshops HDRA 2016 and LINEARITY 2016.
• December 2015. We are excited to announce the launch of Globular (with Krzysztof Bar and Aleks Kissinger), a new online proof assistant for higher category theory. UPDATE: Over 6000 views in 6 months since launch, and 236 person-hours of use!
• November 2015. The proceedings of QPL 2016 (with Chris Heunen and Peter Selinger) are now available.
• September 2015. Preprint "Modular categories as representations of the 3-dimensional bordism 2-category" (with Bruce Bartlett, Chris Douglas and Chris Schommer-Pries) available online, giving the first full proof that 3-dimensional topological quantum field theories are classified in terms of modular tensor categories.
• April 2015. Preprint "Quantum Latin squares and unitary error bases" (with Benjamin Musto) now available, which introduces quantum Latin squares and shows how they can be used to construct new sorts of teleportation protocol. UPDATE: accepted for QIP 2016, the top annual quantum information conference. UPDATE: to appear in Quantum Information & Computation.

Papers

Talks

Public engagement

I find public outreach work exciting and fulfilling, and consider it an important part of an academic career. With David Reutter, I have developed a public engagement workshop, called Qubit.Zone, where participants can explore exciting quantum ideas—including superposition, entanglement and teleportation—using hand-held electronic qubit simulators. A list of all my group's public engagement activity is given below. If you would be interested in having a Qubit.Zone workshop as part of your event, get in touch!