Owen Milner

dblp:441/7263 · DBLP profile ↗
← Back
2ranked-venue papers
0as first author
2since 2021 · last 2026
—ORCID · unresolved

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 2 · 2 since 2021
YearPublicationVenuePosition
2026 A Computer Formalisation of the Serre Finiteness Theorem
Reid Barton, Axel Ljungström, Owen Milner, Anders Mörtberg
LICS3
2026 Classifying 2-Groups in Homotopy Type Theory
abstract
Under the homotopy hypothesis, higher dimensional groups are defined as pointed homotopy types whose homotopy groups vanish outside a certain range. In particular, a 2-group is a pointed connected homotopy 2-type. Classically, 2-groups have two equivalent algebraic descriptions: one in terms of weak monoidal categories and the other in terms of group cohomology. We present these two classifications of pointed connected 2-types in homotopy type theory, thereby providing internal, constructive counterparts to the traditional classifications of 2-groups. Our first classification (in terms of monoidal categories) takes the form of a bicategorical equivalence, while our second is a type equivalence that extends to n-groups for all n ≥ 2. We have mechanized our results in Agda.
Perry Hart, Owen Milner
LICS2