Nick Hu
I am a postdoctoral researcher at the School of
Computer Science in the University of Birmingham, working with Dan
Ghica on string diagrams and the categorical semantics of
programming languages and compilers. My CV can be found here.
I recently completed my DPhil in Computer Science at the University
of Oxford, on the topic of Coherent inverses in
higher-categorical string diagrams under the supervision of Jamie Vicary and Sam
Staton.
If you want to contact me, you can do so by these channels:
Publications
-
Aleksei Tiurin, Chris Barrett, Dan Ghica, and Nick Hu. Equivalence
Hypergraphs: DPO Rewriting for Monoidal E-Graphs. Singapore,
2025.
Proceedings of the 40th Annual ACM/IEEE Symposium
on Logic in Computer Science. To appear (LICS 2025). [arXiv]
-
Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and
Jamie Vicary. homotopy.io: a proof assistant for finitely-presented
globular n-categories.
Tallinn, Estonia, 2024.
9th International Conference on
Formal Structures for Computation and Deduction. https://doi.org/10.4230/LIPIcs.FSCD.2024.30
(FSCD 2024). [arXiv]
-
Nick Hu, and Jamie Vicary. Traced Monoidal Categories as Algebraic
Structures in Prof.
Salzburg, Austria, 2021.
Proceedings of the 37th
Conference on Mathematical Foundations of Programming Semantics. https://doi.org/10.4204/EPTCS.351.6
(MFPS 2021). [arXiv]
-
Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, and Ichiro
Hasuo. Codensity Games for Bisimilarity. Vancouver, Canada,
2019.
Proceedings of the 34th Annual ACM/IEEE Symposium
on Logic in Computer Science. https://doi.org/10.1109/LICS.2019.8785691
(LICS 2019). [journal] [arXiv]
Preprints
Talks
-
sd-visualiser
: interactive string diagram visualisation
for programs.
-
homotopy.io: a proof assistant for finitely-presented globular n-categories.
-
Coherent inverses in higher-categorical string diagrams.
-
Traced Monoidal Categories as Algebraic Structures in Prof.
-
Accelerating Naperian functors.
Events
-
July 2025
-
10th International
Conference on Formal Structures for Computation and Deduction.
-
June 2025
-
40th Annual
ACM/IEEE Symposium on Logic in Computer Science, paper accepted ‘Equivalence Hypergraphs: DPO
Rewriting for Monoidal E-Graphs’.
-
April 2025
-
Thirteenth Symposium
on Compositional Structures, presented talk ‘sd-visualiser:
interactive hypergraph visualisation for programs as string diagrams’.
[slides]
more…
-
March 2025
-
9th Southern
and Midlands Logic Seminar, invited speaker ‘sd-visualiser:
interactive hypergraph visualisation for programs as string diagrams’.
[slides]
-
December 2024
-
Categorical Logic and Higher
Categories workshop.
-
August 2024
-
Visiting the National Institute of
Informatics, Tokyo.
-
Visiting the Research Institute
for Mathematical Sciences, Kyoto University.
-
July 2024
-
Australian
Category Theory Seminar, presented talk ‘Coherent invertibility in
associative n-categories’.
-
Visiting the Centre
for Australian Category Theory, Macquarie University
-
June 2024
-
9th International
Conference on Formal Structures for Computation and Deduction, paper
accepted ‘homotopy.io: a
proof assistant for finitely-presented globular n-categories’.
-
39th Annual
ACM/IEEE Symposium on Logic in Computer Science.
-
13th
International Workshop on Geometric and Topological Methods in Computer
Science, presented talk ‘Coherent invertibility in associative n-categories’. [slides].
-
April 2024
-
Twelfth Symposium on
Compositional Structures, presented talk ‘homotopy.io: a proof
assistant for finitely-presented globular n-categories’. [slides].
-
March 2024
-
Oxford-Topos
meeting.
-
November 2023
-
Fun in the REPL,
presented talk ‘Visualising program dataflow with string diagrams’. [slides]
-
August 2023
-
Pittsposium.
-
January 2023
-
Edinburgh
Diagrams workshop.
-
July 2022
-
Meeting 28
of the Yorkshire and Midlands Category Theory Seminar.
-
Ninth Symposium on
Compositional Structures.
-
July 2022
-
Federated Logic Conference 2022.
-
Research School on
Bicategories, Categorification and Quantum Theory.
-
June 2022
-
10th Conference on
Topology, Algebra, and Categories in Logic.
-
May 2022
-
Meeting 27
of the Yorkshire and Midlands Category Theory Seminar.
-
April 2022
-
22st
Midlands Graduate School in the Foundations of Computing Science.
-
February 2022
-
Logic and Higher
Structures.
-
August 2021
-
37th
Conference on the Mathematical Foundations of Programming Semantics,
presented paper ‘Traced
Monoidal Categories as Algebraic Structures in Prof’.
-
July 2021
-
Fourth International
Conference on Applied Category Theory, local organiser.
-
June 2021
-
Toposes online.
-
April 2021
-
21st
Midlands Graduate School in the Foundations of Computing Science.
-
January 2021
-
2021 Quantum Group Workshop, presented talk ‘Profunctor string
diagrams’. [slides]
-
September 2019
-
Fifth
Symposium on Compositional Structures.
-
July 2019
-
34th Annual
ACM/IEEE Symposium on Logic in Computer Science.
-
September 2018
-
ERATO MMSD Project Camp 2018, presented poster ‘Metric probabilistic
bisimulation games’.
-
July 2018
-
Federated Logic Conference 2018,
student volunteer.
-
November 2017
-
EPSRC Vacation Bursary Poster Event, presented poster ‘Universal
representability for graphical processing units’. [poster]
-
September 2017
-
Second
International Conference on Formal Structures for Computation and
Deduction.
-
22nd ACM SIGPLAN
International Conference on Functional Programming, student
volunteer.
-
January 2017
-
44th ACM SIGPLAN
Symposium on Principles of Programming Languages.
Software
-
homotopy.io
[src]
-
A graphical web-based proof assistant for finitely-presented globular
n-categories, written in Rust,
based on the theory of associative n-categories, which combinatorially
encode n-dimensional string
diagrams. Terms are manipulated as slices of string diagrams in spacial
projection via a point-and-click interface, and can be viewed as 2D
images, an interactive 3D WebGL rendering, or a 4D interactive
animation.
-
sd-visualiser
[src]
-
An interactive tool for visualising string diagrams presented as
hierarchical hypergraphs, written in Rust, which encode terms in a
closed monoidal category and serve as a foundation for building
programming languages. Terms are defined as programs, in either the
implemented toy
sd-lang
language or LLVM IR/MLIR.
Teaching
-
Michaelmas 2025
-
Tutor for Discrete
Mathematics (Catz)
more…
-
Hilary 2024
-
Tutor for Algorithms
and Data Structures (Catz)
-
Michaelmas 2023
-
Admissions interviewer for undergraduate Computer Science & joint
courses (Catz)
-
Hilary 2023
-
Tutor for Algorithms
and Data Structures (Catz)
-
Hilary 2022
-
Tutor for Algorithms
and Data Structures (Catz)
-
Michaelmas 2021
-
Admissions interviewer for undergraduate Computer Science & joint
courses (Catz)
-
Tutor for Categories,
Proofs and Processes and Compilers
(Jesus)
-
Hilary 2021
-
Tutor for Categorical
Quantum Mechanics and Algorithms
and Data Structures (Catz)
-
Michaelmas 2020
-
Admissions interviewer for undergraduate Computer Science & joint
courses (Catz)
-
Hilary 2020
-
Tutor for Categorical
Quantum Mechanics and Algorithms
and Data Structures (Catz)
-
Michaelmas 2019
-
Admissions interviewer for undergraduate Computer Science & joint
courses (Catz)
-
Tutor for Quantum
Computer Science and Computer-Aided
Formal Verification
-
TA for Computer-Aided
Formal Verification
-
Practical demonstrator for Functional
Programming and Principles
of Programming Languages
-
Hilary 2019
-
Practical demonstrator for Imperative
Programming I&II and Design
and Analysis of Algorithms
-
TA for Functional
Programming (Software Engineering Department)
-
Michaelmas 2018
-
MAT marker
-
Practical demonstrator for Functional
Programming and Compilers
Miscellaneous
notes
Last updated: 20250721175239