diff --git a/quox.bib b/quox.bib index 2729e4b..f46e25d 100644 --- a/quox.bib +++ b/quox.bib @@ -13,8 +13,7 @@ pages = {462--490}, publisher = {Springer}, year = {2021}, -% url = {https://doi.org/10.1007/978-3-030-72019-3\_17}, - url = {https://arxiv.org/abs/2010.13163}, + url = {https://doi.org/10.1007/978-3-030-72019-3\_17}, doi = {10.1007/978-3-030-72019-3\_17} } @@ -40,7 +39,7 @@ @inproceedings{qtt, author = {Robert Atkey}, editor = {Anuj Dawar and - Erich Gr{\"{a}}del}, + Erich Grädel}, title = {Syntax and Semantics of Quantitative Type Theory}, booktitle = {Proceedings of the 33rd Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS} 2018, Oxford, UK, July 09-12, 2018}, @@ -73,7 +72,7 @@ } @article{ott-good, - author = {Lo{\"{\i}}c Pujet and Nicolas Tabareau}, + author = {Loïc Pujet and Nicolas Tabareau}, title = {Observational equality: now for good}, journal = {Proc. {ACM} Program. Lang.}, volume = {6}, @@ -93,7 +92,7 @@ series = {LIPIcs}, volume = {131}, pages = {31:1--31:25}, - publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, + publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, year = {2019}, % url = {https://doi.org/10.4230/LIPIcs.FSCD.2019.31}, url = {https://arxiv.org/pdf/1904.08562.pdf}, @@ -104,7 +103,7 @@ % NbE @article{nbe-mltt, - title = {Normalization by Evaluation for Martin-L\"of Type Theory with + title = {Normalization by Evaluation for Martin-Löf Type Theory with One Universe}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {173}, @@ -113,8 +112,8 @@ note = {Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII)}, issn = {1571-0661}, - doi = {https://doi.org/10.1016/j.entcs.2007.02.025}, - url = {https://www.sciencedirect.com/science/article/pii/S1571066107000977}, + doi = {10.1016/j.entcs.2007.02.025}, + url = {https://doi.org/10.1016/j.entcs.2007.02.025}, author = {Andreas Abel and Klaus Aehlig and Peter Dybjer}, keywords = {Dependent Types, Domain Semantics, Normalization by Evaluation, Type Theory, Universe} @@ -122,7 +121,7 @@ @inproceedings{nbe-mltt-eq, author = {Andreas Abel and Thierry Coquand and Peter Dybjer}, - title = {Normalization by Evaluation for Martin-L\"of Type Theory with Typed + title = {Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements}, booktitle = {22nd {IEEE} Symposium on Logic in Computer Science ({LICS} 2007)}, @@ -145,7 +144,7 @@ publisher = {{ACM}}, year = {2019}, % url = {https://doi.org/10.1145/3354166.3354168}, - url = {https://www.cse.chalmers.se/~abela/ppdp19.pdf}, + url = {https://research.chalmers.se/publication/516703/file/516703_Fulltext.pdf}, doi = {10.1145/3354166.3354168} } @@ -154,8 +153,7 @@ title = {Normalization by Evaluation: Dependent Types and Impredicativity}, year = {2013}, type = {Habilitation thesis}, - school = {Institut f\"ur Informatik, - Ludwig-Maximilians-Universit\"at M\"unchen}, + school = {Institut für Informatik, Ludwig-Maximilians-Universität München}, url = {https://www.cse.chalmers.se/~abela/habil.pdf} } @@ -163,22 +161,23 @@ author = {Andreas Abel and James Chapman}, editor = {Paul Levy and Neel Krishnaswami}, title = {Normalization by Evaluation in the Delay Monad: - {A} Case Study for Coinduction via Copatterns and Sized Types}, + A Case Study for Coinduction via Copatterns and Sized Types}, booktitle = {Proceedings 5th Workshop on Mathematically Structured - Functional Programming (MSFP 2014)}, + Functional Programming ({MSFP} 2014)}, series = {{EPTCS}}, volume = {153}, pages = {51--67}, year = {2014}, -% url = {https://doi.org/10.4204/EPTCS.153.4}, - url = {https://www.cse.chalmers.se/~abela/eptcs14.pdf}, + url = {https://doi.org/10.4204/EPTCS.153.4}, doi = {10.4204/EPTCS.153.4} } % Misc type stuff @article{calf, - author = {Niu, Yue and Sterling, Jonathan and Grodin, Harrison and + author = {Niu, Yue and + Sterling, Jonathan and + Grodin, Harrison and Harper, Robert}, title = {A Cost-Aware Logical Framework}, year = {2022}, @@ -197,13 +196,57 @@ reasoning, recurrence relations, modal type theory} } +@article{mugen, + author = {Hou (Favonia), Kuen-Bang and Angiuli, Carlo and Mullanix, Reed}, + title = {An Order-Theoretic Analysis of Universe Polymorphism}, + year = {2023}, + issue_date = {January 2023}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + volume = {7}, + number = {POPL}, + url = {https://doi.org/10.1145/3571250}, + doi = {10.1145/3571250}, + abstract = { + We present a novel formulation of universe polymorphism in dependent type + theory in terms of monads on the category of strict partial orders, and a + novel algebraic structure, displacement algebras, on top of which one can + implement a generalized form of McBride’s “crude but effective + stratification” scheme for lightweight universe polymorphism. We give some + examples of exotic but consistent universe hierarchies, and prove that every + universe hierarchy in our sense can be embedded in a displacement algebra + and hence implemented via our generalization of McBride’s scheme. Many of + our technical results are mechanized in Agda, and we have an OCaml library + for universe levels based on displacement algebras, for use in proof + assistant implementations. + }, + journal = {Proc. ACM Program. Lang.}, + month = {jan}, + articleno = {57}, + numpages = {27}, + keywords = {universes, type theory, universe polymorphism} +} + +@article{bidi, + author = {Jana Dunfield and Neel Krishnaswami}, + title = {Bidirectional Typing}, + journal = {{ACM} Comput. Surv.}, + volume = {54}, + number = {5}, + pages = {98:1--98:38}, + year = {2022}, + url = {https://doi.org/10.1145/3450952}, + doi = {10.1145/3450952}, +} + + % Misc implementation @article{expl-sub, - author = {Mart{\'{\i}}n Abadi and + author = {Martín Abadi and Luca Cardelli and Pierre{-}Louis Curien and - Jean{-}Jacques L{\'{e}}vy}, + Jean{-}Jacques Lévy}, title = {Explicit Substitutions}, journal = {J. Funct. Program.}, volume = {1}, @@ -245,34 +288,3 @@ url = {https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf}, doi = {10.1007/s10990-006-0480-6}, } - -@article{mugen, - author = {Hou (Favonia), Kuen-Bang and Angiuli, Carlo and Mullanix, Reed}, - title = {An Order-Theoretic Analysis of Universe Polymorphism}, - year = {2023}, - issue_date = {January 2023}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - volume = {7}, - number = {POPL}, - url = {https://doi.org/10.1145/3571250}, - doi = {10.1145/3571250}, - abstract = { - We present a novel formulation of universe polymorphism in dependent type - theory in terms of monads on the category of strict partial orders, and a - novel algebraic structure, displacement algebras, on top of which one can - implement a generalized form of McBride’s “crude but effective - stratification” scheme for lightweight universe polymorphism. We give some - examples of exotic but consistent universe hierarchies, and prove that every - universe hierarchy in our sense can be embedded in a displacement algebra - and hence implemented via our generalization of McBride’s scheme. Many of - our technical results are mechanized in Agda, and we have an OCaml library - for universe levels based on displacement algebras, for use in proof - assistant implementations. - }, - journal = {Proc. ACM Program. Lang.}, - month = {jan}, - articleno = {57}, - numpages = {27}, - keywords = {universes, type theory, universe polymorphism} -}