Nick Hu
I am a DPhil student at the Department of
Computer Science in the University of Oxford, and I have interests in
category theory and its applications to computer science. Please see my departmental
webpage for more details. My CV can be found here.
If you want to contact me, you can do so by these channels (in
descending order of checking frequency):
Publications
Preprints
- Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru,
and Jamie Vicary. homotopy.io: a proof assistant
for finitely-presented globular n-categories.
Submitted to the 9th International Conference on Formal Structures for
Computation and Deduction, Tallinn, Estonia, 2024.
- Nick Hu, Calin Tataru, and Jamie Vicary. Coherent invertibility in associative
n-categories.
Submitted to the 39th Annual ACM/IEEE Symposium on Logic in Computer
Science, Tallinn, Estonia, 2024.
Talks
- ‘Visualising program dataflow with string diagrams’, November 2023.
13th South of England Regional Programming Language Seminar/Fun in the
REPL. [slides]
- homotopy.io: a proof assistant for finitely-presented globular n-categories
- ERATO MMSD Colloquium. [slides]
- Midlands Graduate School 2022 student presentations.
- Traced Monoidal
Categories as Algebraic Structures in Prof,
2021.
- 37th Conference on Mathematical Foundations of Programming
Semantics. [slides]
- Category Theory 20→21. [video]
- ‘Accelerating Naperian functors’, September 2017. 7th South of
England Regional Programming Language Seminar. [slides]
Events
-
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.
more…
-
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
language or LLVM MLIR.
Miscellaneous
notes
Last updated: Mon, 18 Mar 2024 17:56:02 +0000