I am a postdoctoral fellow in the Department of Mathematics and Statistics at Dalhousie University working with Peter Selinger and Julien Ross. My research involves a wide range of areas of mathematics including higher category theory, homotopy type theory, and quantum computing.
Previously, I did my doctorate at the University of Oxford under the supervision of Kobi Kremnitzer and Jamie Vicary.
In this article, we report the development of a resource estimation pipeline that explicitly compiles quantum circuits expressed using the Clifford+T gate set into a lower level instruction set made out of fault-tolerant operations on the surface code. The cadence of magic state requests from the compiled circuit enables the optimization of magic state distillation and storage requirements in a post-hoc analysis. To compile logical circuits, we build upon the open-source Lattice Surgery Compiler, which is extensible to different surface code compilation strategies within the lattice surgery paradigm. The revised compiler operates in two stages: the first translates logical gates into an abstract, layout-independent instruction set; the second compiles these into local lattice surgery instructions that are allocated to hardware tiles according to a specified resource layout. In the second stage, parallelism in the logical circuit is translated into parallelism within the fault-tolerant layer while avoiding resource contention, which allows the compiler to find a realistic number of logical time-steps to execute the circuit. The revised compiler also improves the handling of magic states by allowing users to specify dedicated hardware tiles at which magic states are replenished according to a user-specified rate, which allows resource costs from the logical computation to be considered independently from magic state distillation and storage. We demonstrate the applicability of our resource estimation pipeline to large, practical quantum circuits by providing resource estimates for the ground state estimation of molecules. We find that, unless carefully considered, the resource costs of magic state storage can dominate in real circuits which have variable magic state consumption rates.
arxiv
Computads for weak ω-categories as an inductive type
We give a new description of computads for weak globular ω-categories by giving an explicit inductive definition of the free words. This yields a new understanding of computads, and allows a new definition of ω-category that avoids the technology of globular operads. Our framework permits direct proofs of important results via structural induction, and we use this to give new proofs that every ω-category is equivalent to a free one, and that the category of computads with variable-to-variable maps is a presheaf topos, giving a direct description of the index category. We prove that our resulting definition of ω-category agrees with that of Batanin and Leinster and that the induced notion of cofibrant replacement for ω-categories coincides with that of Garner.
We introduce various notions of globular multicategory with homomorphism types. We develop a higher dimensional modules construction that constructs globular multicategories with strict homomorphism types. We illustrate how this construction is related to iterated enrichment. We show how various collections of “higher category-like” objects give rise to globular multicategories with homomorphism types. We show how these structures suggest a new globular approach to the semantics of (directed) homotopy type theory.