this repo has no description
jonmsterling.com
1@INPROCEEDINGS {pugh-sterling-2025,
2author = { Pugh, Leoni and Sterling, Jonathan },
3booktitle = { 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) },
4title = {{ When is the partial map classifier a Sierpiński cone? }},
5year = {2025},
6volume = {},
7ISSN = {},
8pages = {718-731},
9abstract = { We study the relationship between partial map classifiers, Sierpiński cones, and axioms for synthetic higher categories and domains within univalent foundations. In particular, we show that synthetic ∞-categories are closed under partial map classifiers assuming Phoa’s principle, and we isolate a new reflective subuniverse of types within which the Sierpiński cone (a lax colimit) can be computed as a partial map classifier by strengthening the Segal condition. },
10keywords = {Computer science;Logic},
11doi = {10.1109/LICS65433.2025.00060},
12url = {https://doi.ieeecomputersociety.org/10.1109/LICS65433.2025.00060},
13publisher = {IEEE Computer Society},
14address = {Los Alamitos, CA, USA},
15month =Jun}
16
17@misc{vickers-categories-2008-elephant,
18 title = {Re: Heyting algebras and Wikipedia},
19 note = {A message from Steve Vickers to the \emph{Categories} mailing list},
20 url = {https://mta.ca/~cat-dist/archive/2008/08-3},
21 year = {2008},
22 month = mar,
23 day = {9},
24 author = {Vickers, Steve}
25}
26
27@phdthesis{gratzer-2023-thesis,
28title = {Syntax and semantics of modal type theory},
29author = {Gratzer, Daniel},
30school = {Aarhus University},
31year = {2023},
32url = {https://www.danielgratzer.com/papers/phd-thesis.pdf},
33}
34
35@inproceedings{10.1145/3373718.3394736, author = {Gratzer, Daniel and Kavvos, G. A. and Nuyts, Andreas and Birkedal, Lars}, title = {Multimodal Dependent Type Theory}, year = {2020}, isbn = {9781450371049}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3373718.3394736}, doi = {10.1145/3373718.3394736}, abstract = {We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion --- demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.}, booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science}, pages = {492–506}, numpages = {15}, keywords = {Modal types K@dependent types, categorical semantics, gluing, guarded recursion}, location = {Saarbr\"{u}cken, Germany}, series = {LICS '20} }
36
37
38
39@inproceedings{10.1145/3531130.3532398, author = {Gratzer, Daniel}, title = {Normalization for Multimodal Type Theory}, year = {2022}, isbn = {9781450393515}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3531130.3532398}, doi = {10.1145/3531130.3532398}, abstract = {We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof follows from a generalization of synthetic Tait computability—an abstract approach to gluing proofs—to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a significant case study of MTT.}, booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, articleno = {2}, numpages = {13}, keywords = {type theory, normalization, modalities, modal type theory, categorical semantics, Artin gluing}, location = {Haifa, Israel}, series = {LICS '22} }
40
41
42@INPROCEEDINGS{11186122,
43author={Gratzer, Daniel and Weinberger, Jonathan and Buchholtz, Ulrik},
44booktitle={2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
45title={The Yoneda embedding in simplicial type theory},
46year={2025},
47volume={},
48number={},
49pages={127-142},
50keywords={Computer science;Complexity theory;Logic;type theory;category theory;modal dependent type theory;infinity category theory;homotopy type theory},
51doi={10.1109/LICS65433.2025.00017}}
52
53@misc{sterling2025domainsclassifyingtopoi,
54 title={Domains and Classifying Topoi},
55 author={Jonathan Sterling and Lingyuan Ye},
56 year={2025},
57 eprint={2505.13096},
58 archivePrefix={arXiv},
59 primaryClass={cs.LO},
60 url={https://arxiv.org/abs/2505.13096},
61}
62
63@article{rijke-shulman-spitters:2020,
64 author = {Rijke, Egbert and Shulman, Michael and Spitters, Bas},
65 year = {2020},
66 month = jan,
67 doi = {10.23638/LMCS-16(1:2)2020},
68 issue = {1},
69 journal = lmcs,
70 pages = {2:1--2:79},
71 title = {Modalities in homotopy type theory},
72 volume = {16},
73}
74
75
76@article{riehl-shulman:2017,
77 author = {Riehl, Emily and Shulman, Michael},
78 url = {https://journals.mq.edu.au/index.php/higher_structures/article/view/36},
79 year = {2017},
80 eprint = {1705.07442},
81 eprintclass = {math.CT},
82 eprinttype = {arXiv},
83 issue = {1},
84 journal = {Higher Structures},
85 pages = {147--224},
86 title = {A type theory for synthetic $\infty$-categories},
87 volume = {1},
88}
89
90@inproceedings{fiore-rosolini:1997:cpos,
91 author = {Fiore, Marcelo P. and Rosolini, Giuseppe},
92 editor = {Brookes, Stephen D. and Mislove, Michael W.},
93 publisher = {Elsevier},
94 booktitle = {Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, {MFPS} 1997, Carnegie Mellon University, Pittsburgh, PA, USA, March 23-26, 1997},
95 year = {1997},
96 doi = {10.1016/S1571-0661(05)80165-3},
97 pages = {133--150},
98 series = entcs,
99 title = {The category of cpos from a synthetic viewpoint},
100 volume = {6},
101}
102
103@inproceedings{hyland:1991,
104 author = {Hyland, J. M. E.},
105 editor = {Carboni, Aurelio and Pedicchio, Maria Cristina and Rosolini, Guiseppe},
106 address = {Berlin, Heidelberg},
107 publisher = {Springer Berlin Heidelberg},
108 booktitle = {Category Theory},
109 year = {1991},
110 isbn = {978-3-540-46435-8},
111 pages = {131--156},
112 title = {First steps in synthetic domain theory},
113}
114
115@unpublished{taylor:2000,
116 author = {Taylor, Paul},
117 url = {http://www.paultaylor.eu/ASD/nonagr.pdf},
118 year = {2000},
119 note = {Presented at \emph{Category Theory 2000} in Como},
120 title = {Non-{Artin} gluing in recursion theory and lifting in abstract {Stone} duality},
121}
122
123@book{hottbook,
124 author = {{Univalent Foundations Program}, The},
125 address = {Institute for Advanced Study},
126 publisher = {\url{https://homotopytypetheory.org/book}},
127 year = {2013},
128 title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
129}
130
131
132@article{taylor:2006,
133 author = {Taylor, Paul},
134 url = {https://lmcs.episciences.org/2255},
135 year = {2006},
136 month = mar,
137 doi = {10.2168/LMCS-2(1:1)2006},
138 issue = {1},
139 journal = {Logical Methods in Computer Science},
140 title = {{Computably Based Locally Compact Spaces}},
141 volume = {2},
142}
143
144@article{taylor:2002,
145 title = {Sober spaces and continuations},
146 author = {Taylor, Paul},
147 journal = {Theory and Applications of Categories},
148 volume = {10},
149 year = {2002},
150 issue = {12},
151}
152
153
154@phdthesis{rosolini:1986,
155 author = {Rosolini, Guiseppe},
156 school = {University of Oxford},
157 year = {1986},
158 title = {Continuity and effectiveness in topoi},
159}
160
161@article{dyckhoff-tholen:1987,
162 author = {Dyckhoff, Roy and Tholen, Walter},
163 year = {1987},
164 doi = {10.1016/0022-4049(87)90124-1},
165 issn = {0022-4049},
166 journal = jpaa,
167 number = {1},
168 pages = {103--116},
169 title = {Exponentiable morphisms, partial products and pullback complements},
170 volume = {49},
171}
172
173@incollection{johnstone:1992,
174 author = {Johnstone, Peter T.},
175 editor = {Fourman, M. P. and Johnstone, Peter T. and Pitts, A. M.},
176 publisher = cup,
177 booktitle = {Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991},
178 year = {1992},
179 doi = {10.1017/CBO9780511525902.018},
180 pages = {315--339},
181 series = {London Mathematical Society Lecture Note Series},
182 title = {Partial products, bagdomains and hyperlocal toposes},
183}
184
185@article{johnstone:1993,
186 author = {Johnstone, Peter T.},
187 year = {1993},
188 month = jun,
189 doi = {10.1007/BF00880041},
190 journal = {Applied Categorical Structures},
191 number = {2},
192 pages = {141--179},
193 title = {Fibrations and partial products in a 2-category},
194 volume = {1},
195}