Search Results

Documents authored by Milner, Owen

Document
DOI: 10.4230/LIPIcs.TYPES.2025.1
Choice Principles and Hypercompletion in HoTT

Authors: Owen Milner

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

Abstract
Building on work of Anel and Barton [M. Anel and R. Barton, 2024], we will introduce the construction of a hypercompletion modality [E. Rijke et al., 2020] in HoTT under the assumption that countable choice holds. Central results have been formalized in Cubical Agda and will be referenced where appropriate.
Cite as

Owen Milner. Choice Principles and Hypercompletion in HoTT. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{milner:LIPIcs.TYPES.2025.1,
  author =	{Milner, Owen},
  title =	{{Choice Principles and Hypercompletion in HoTT}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{1:1--1:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.1},
  URN =		{urn:nbn:de:0030-drops-270193},
  doi =		{10.4230/LIPIcs.TYPES.2025.1},
  annote =	{Keywords: HoTT, hypercompletion, modalities}
}
Artifact
Software
DOI: 10.4230/artifacts.26876
A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation)

Authors: Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg

Abstract
Cite as

Reid Barton, Axel Ljungström, Owen Milner, Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{SerreFiniteness,
   title = {{A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation)}}, 
   author = {Barton, Reid and Ljungstr\"{o}m, Axel and Milner, Owen and M\"{o}rtberg, Anders},
   note = {Software, ForCUTT project, ERC advanced grant 101053291, Knut & Alice Wallenberg Foundation’s Program for Mathematics, This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009, PI Steve Awodey, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:5c9314da89014673a22878132bb63cfc42ccfa73;origin=https://github.com/CMU-HoTT/serre-finiteness;visit=swh:1:snp:0f3bfe0f67361dc33562f0fc15b80309b3290611;anchor=swh:1:rev:79f3150942a129eb544004adcdef4b17244d5ed4}{\texttt{swh:1:dir:5c9314da89014673a22878132bb63cfc42ccfa73}} (visited on 2026-07-09)},
   url = {https://github.com/CMU-HoTT/serre-finiteness},
   doi = {10.4230/artifacts.26876},
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.16
A Computer Formalisation of the Serre Finiteness Theorem

Authors: Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
Few constructions in mathematics are as elusive as the homotopy groups of spheres. These groups, which intuitively measure n-dimensional loops on m-dimensional spheres, appear at first glance to be almost completely random - an unfortunate fact, seeing as they constitute one of the fundamental building blocks of algebraic topology and homotopy theory. However, the situation is not completely hopeless: in 1951, Serre proved his celebrated finiteness theorem, which says that these groups are almost always finite abelian groups, except in two classes of special cases when they also contain copies of the integers. In a recent paper, Barton and Campion proved a variation of this result in homotopy type theory (HoTT) - an extension of Martin-Löf type theory, particularly suitable for reasoning about and formalising algebraic topology and homotopy theory. Their result shows that the homotopy groups of spheres are all finitely presented - and constructively so. Prior to this proof, only low-dimensional homotopy groups of spheres had been computed in HoTT. This made it a major breakthrough for HoTT as a foundation and, as such, the immediate target of a full-scale formalisation project. In this paper, we present the outcome of this project: a complete formalisation of Barton and Campion’s proof of the Serre finiteness theorem in Cubical Agda, a constructive proof assistant implementing a cubical flavour of HoTT. In the light of the constructivity of Cubical Agda, we discuss the prospect of running the algorithm provided by our formalisation in order to compute concrete homotopy groups of spheres.
Cite as

Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barton_et_al:LIPIcs.LICS.2026.16,
  author =	{Barton, Reid and Ljungstr\"{o}m, Axel and Milner, Owen and M\"{o}rtberg, Anders},
  title =	{{A Computer Formalisation of the Serre Finiteness Theorem}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{16:1--16:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.16},
  URN =		{urn:nbn:de:0030-drops-268031},
  doi =		{10.4230/LIPIcs.LICS.2026.16},
  annote =	{Keywords: Homotopy type theory, synthetic homotopy theory, formalisation of mathematics, constructive mathematics}
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.55
Classifying 2-Groups in Homotopy Type Theory

Authors: Perry Hart and Owen Milner

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

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.
Cite as

Perry Hart and Owen Milner. Classifying 2-Groups in Homotopy Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 55:1-55:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{hart_et_al:LIPIcs.LICS.2026.55,
  author =	{Hart, Perry and Milner, Owen},
  title =	{{Classifying 2-Groups in Homotopy Type Theory}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{55:1--55:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.55},
  URN =		{urn:nbn:de:0030-drops-268428},
  doi =		{10.4230/LIPIcs.LICS.2026.55},
  annote =	{Keywords: homotopy type theory, synthetic homotopy theory, 2-group, higher inductive type, bicategory, higher group, cohomology}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact