% quantitative/modal stuff {{{1

@inproceedings{grtt,
  author    = {Moon, Benjamin and
               Eades, III, Harley and
               Orchard, Dominic},
  editor    = {Yoshida, Nobuko},
  title     = {Graded Modal Dependent Type Theory},
  booktitle = {Programming Languages and Systems:
               30th European Symposium on Programming, ({ESOP} 2021)},
  series    = {Lecture Notes in Computer Science},
  volume    = {12648},
  pages     = {462--490},
  publisher = {Springer},
  year      = {2021},
  url       = {https://doi.org/10.1007/978-3-030-72019-3\_17},
  doi       = {10.1007/978-3-030-72019-3\_17}
}

@article{granule,
  author  = {Dominic Orchard and Vilem{-}Benjamin Liepelt and Harley Eades III},
  title   = {Quantitative program reasoning with graded modal types},
  journal = {Proceedings of the {ACM} on Programming Languages},
  volume  = {3},
  number  = {{ICFP}},
  pages   = {110:1--110:30},
  year    = {2019},
  url     = {https://doi.org/10.1145/3341714},
  doi     = {10.1145/3341714},
}

@inproceedings{nuttin,
  author    = {Conor McBride},
  editor    = {Sam Lindley and
               Conor McBride and
               Philip W. Trinder and
               Donald Sannella},
  title     = {I Got Plenty o' Nuttin'},
  booktitle = {A List of Successes That Can Change the World - Essays Dedicated to
               Philip Wadler on the Occasion of His 60th Birthday},
  series    = {Lecture Notes in Computer Science},
  volume    = {9600},
  pages     = {207--233},
  publisher = {Springer},
  year      = {2016},
% url       = {https://doi.org/10.1007/978-3-319-30936-1\_12},
  url       = {https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf},
  doi       = {10.1007/978-3-319-30936-1\_12}
}

@inproceedings{qtt,
  author    = {Robert Atkey},
  editor    = {Anuj Dawar and
               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},
  pages     = {56--65},
  publisher = {{ACM}},
  year      = {2018},
% url       = {https://doi.org/10.1145/3209108.3209189},
  url       = {https://bentnib.org/quantitative-type-theory.pdf},
  doi       = {10.1145/3209108.3209189}
}

@article{frac-uniq,
  author    = {Marshall, Daniel and Orchard, Dominic},
  title     = {Functional Ownership through Fractional Uniqueness},
  year      = {2024},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  volume    = {8},
  number    = {OOPSLA1},
  url       = {https://doi.org/10.1145/3649848},
  doi       = {10.1145/3649848},
  journal   = {Proc. ACM Program. Lang.},
}

@article{rustbelt,
  author    = {Jung, Ralf and
               Jourdan, Jacques-Henri and
               Krebbers, Robbert and
               Dreyer, Derek},
  title     = {{RustBelt}:
               securing the foundations of the {R}ust programming language},
  year      = {2017},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  volume    = {2},
  number    = {POPL},
  url       = {https://doi.org/10.1145/3158154},
  doi       = {10.1145/3158154},
  journal   = {Proc. ACM Program. Lang.},
}

@article{lightweight-rust,
  author    = {Pearce, David J.},
  title     = {A Lightweight Formalism for Reference Lifetimes
               and Borrowing in Rust},
  year      = {2021},
  publisher = {Association for Computing Machinery},
  volume    = {43},
  number    = {1},
  url       = {https://doi.org/10.1145/3443420},
  doi       = {10.1145/3443420},
  journal   = {ACM Trans. Program. Lang. Syst.},
}

@misc{oxide,
  title         = {Oxide: The Essence of Rust},
  author        = {Aaron Weiss and
                   Olek Gierczak and
                   Daniel Patterson and
                   Amal Ahmed},
  year          = {2021},
  eprint        = {1903.00982},
  archivePrefix = {arXiv},
  primaryClass  = {cs.PL}
}

@inproceedings{frac-perms,
  author       = {John Boyland},
  editor       = {Radhia Cousot},
  title        = {Checking Interference with Fractional Permissions},
  booktitle    = {Static Analysis, 10th International Symposium, {SAS} 2003,
                  San Diego, CA, USA, June 11-13, 2003, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {2694},
  pages        = {55--72},
  publisher    = {Springer},
  year         = {2003},
  url          = {https://doi.org/10.1007/3-540-44898-5\_4},
  doi          = {10.1007/3-540-44898-5\_4},
}

@inproceedings{linexp-graded,
  title = {Linear Exponentials as Graded Modal Types},
  author = {Hughes, Jack and
            Marshall, Daniel and
            Wood, James and
            Orchard, Dominic},
  url = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271465},
  booktitle = {5th International Workshop on
               Trends in Linear Logic and Applications ({TLLA} 2021)},
  year = {2021},
  month = Jun,
}

@inproceedings{alms,
  author    = {Tov, Jesse A. and Pucella, Riccardo},
  title     = {Practical affine types},
  year      = {2011},
  publisher = {Association for Computing Machinery},
  url       = {https://users.cs.northwestern.edu/~jesse/pubs/alms/tovpucella-alms.pdf},
  doi       = {10.1145/1926385.1926436},
  booktitle = {Proceedings of the 38th Annual ACM SIGPLAN-SIGACT
               Symposium on Principles of Programming Languages},
}

@inproceedings{rrr,
  author    = {Daniel Marshall and Dominic Orchard},
  editor    = {Marco Carbone and Rumyana Neykova},
  title     = {Replicate, Reuse, Repeat: Capturing Non-Linear Communication
               via Session Types and Graded Modal Types},
  booktitle = {Proceedings of the 13th International Workshop on Programming
               Language Approaches to Concurrency and Communication-cEntric
               Software, PLACES@ETAPS 2022, Munich, Germany, 3rd April 2022},
  series    = {{EPTCS}},
  volume    = {356},
  pages     = {1--11},
  year      = {2022},
  url       = {https://arxiv.org/abs/2203.12875},
  doi       = {10.4204/EPTCS.356.1},
}


% observational stuff {{{1

@inproceedings{ott-now,
  author    = {Thorsten Altenkirch and
               Conor McBride and
               Wouter Swierstra},
  editor    = {Aaron Stump and
               Hongwei Xi},
  title     = {Observational equality, now!},
  booktitle = {Proceedings of the {ACM} Workshop Programming Languages meets Program
               Verification, {PLPV} 2007, Freiburg, Germany, October 5, 2007},
  pages     = {57--68},
  publisher = {{ACM}},
  year      = {2007},
% url       = {https://doi.org/10.1145/1292597.1292608},
  url       = {https://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf},
  doi       = {10.1145/1292597.1292608}
}

@article{ott-good,
  author  = {Loïc Pujet and Nicolas Tabareau},
  title   = {Observational equality: now for good},
  journal = {Proc. {ACM} Program. Lang.},
  volume  = {6},
  number  = {{POPL}},
  pages   = {1--27},
  year    = {2022},
  url     = {https://doi.org/10.1145/3498693},
  doi     = {10.1145/3498693},
}

@inproceedings{xtt,
  author    = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
  editor    = {Herman Geuvers},
  title     = {Cubical Syntax for Reflection-Free Extensional Equality},
  booktitle = {4th International Conference on Formal Structures for Computation
               and Deduction, {FSCD} 2019, June 24-30, 2019, Dortmund, Germany},
  series    = {LIPIcs},
  volume    = {131},
  pages     = {31:1--31:25},
  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},
  doi       = {10.4230/LIPIcs.FSCD.2019.31}
}

@unpublished{cubical-ott,
  author = {James Chapman and Fredrik Nordvall Forsberg and Conor {McBride}},
  title  = {The Box of Delights (Cubical Observational Type Theory)},
  year   = {2018},
  url    = {https://github.com/msp-strath/platypus/blob/138daf7/January18/doc/CubicalOTT/CubicalOTT.pdf},
}


% NbE {{{1

@article{nbe-mltt,
  title    = {Normalization by Evaluation for Martin-Löf Type Theory with
              One Universe},
  journal  = {Electronic Notes in Theoretical Computer Science},
  volume   = {173},
  pages    = {17-39},
  year     = {2007},
  note     = {Proceedings of the 23rd Conference on the Mathematical Foundations
              of Programming Semantics (MFPS XXIII)},
  issn     = {1571-0661},
  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}
}

@inproceedings{nbe-mltt-eq,
  author    = {Andreas Abel and Thierry Coquand and Peter Dybjer},
  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)},
  pages     = {3--12},
  publisher = {{IEEE} Computer Society},
  year      = {2007},
% url       = {https://doi.org/10.1109/LICS.2007.33},
  url       = {https://www.cse.chalmers.se/~abela/lics07.pdf},
  doi       = {10.1109/LICS.2007.33}
}

@inproceedings{nbe-cbpv,
  author    = {Andreas Abel and Christian Sattler},
  editor    = {Ekaterina Komendantskaya},
  title     = {Normalization by Evaluation for Call-By-Push-Value and Polarized
               Lambda Calculus},
  booktitle = {Proceedings of the 21st International Symposium on Principles and
               Practice of Programming Languages ({PPDP} 2019)},
  pages     = {3:1--3:12},
  publisher = {{ACM}},
  year      = {2019},
% url       = {https://doi.org/10.1145/3354166.3354168},
  url       = {https://research.chalmers.se/publication/516703/file/516703_Fulltext.pdf},
  doi       = {10.1145/3354166.3354168}
}

@phdthesis{nbe-habil,
  author = {Andreas Abel},
  title  = {Normalization by Evaluation: Dependent Types and Impredicativity},
  year   = {2013},
  type   = {Habilitation thesis},
  school = {Institut für Informatik, Ludwig-Maximilians-Universität München},
  url    = {https://www.cse.chalmers.se/~abela/habil.pdf}
}

@inproceedings{nbe-delay,
  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},
  booktitle = {Proceedings 5th Workshop on Mathematically Structured
               Functional Programming ({MSFP} 2014)},
  series    = {{EPTCS}},
  volume    = {153},
  pages     = {51--67},
  year      = {2014},
  url       = {https://doi.org/10.4204/EPTCS.153.4},
  doi       = {10.4204/EPTCS.153.4}
}

% Misc type stuff {{{1

@article{calf,
  author = {Niu, Yue and
            Sterling, Jonathan and
            Grodin, Harrison and
            Harper, Robert},
  title = {A Cost-Aware Logical Framework},
  year = {2022},
  publisher = {Association for Computing Machinery},
  volume = {6},
  number = {POPL},
  url = {https://doi.org/10.1145/3498670},
  doi = {10.1145/3498670},
  journal = {Proc. {ACM} Program. Lang.},
  month = {jan},
  articleno = {9},
  numpages = {31},
  keywords = {amortized analysis, phase distinction, algorithm analysis, cost
    models, proof assistants, mechanized proof, parallel algorithms,
    noninterference, intensional property, behavioral verification, equational
    reasoning, recurrence relations, modal type theory}
}

@misc{crude,
  author = {McBride, Conor},
  title  = {Crude but effective stratification},
  url    = {https://personal.cis.strath.ac.uk/conor.mcbride/Crude.pdf},
  note   = {slides}
}

@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{qiit-containers,
  author = {Thorsten Altenkirch and Stefania Damato},
  title  = {Specifying {QIIT}s using Containers},
  howpublished = {\url{https://hott-uf.github.io/2023/HoTTUF_2023_paper_8931.pdf}},
  date = {2023},
}

@inproceedings{multimodal,
  author       = {Daniel Gratzer and
                  G. A. Kavvos and
                  Andreas Nuyts and
                  Lars Birkedal},
  editor       = {Holger Hermanns and
                  Lijun Zhang and
                  Naoki Kobayashi and
                  Dale Miller},
  title        = {Multimodal Dependent Type Theory},
  booktitle    = {{LICS} '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer
                  Science, Saarbrücken, Germany, July 8--11, 2020},
  pages        = {492--506},
  publisher    = {{ACM}},
  year         = {2020},
  url          = {https://doi.org/10.1145/3373718.3394736},
  doi          = {10.1145/3373718.3394736},
}

@inproceedings{recursion_modality,
  author       = {Adrien Guatto},
  editor       = {Anuj Dawar and
                  Erich Grädel},
  title        = {A Generalized Modality for Recursion},
  booktitle    = {{LICS} '18: 33rd Annual {ACM/IEEE} Symposium on
                  Logic in Computer Science, Oxford, UK, July 09--12, 2018},
  pages        = {482--491},
  publisher    = {{ACM}},
  year         = {2018},
% url          = {https://doi.org/10.1145/3209108.3209148},
  url          = {https://arxiv.org/pdf/1805.11021.pdf},
  doi          = {10.1145/3209108.3209148},
}

@inproceedings{clocks_are_ticking,
  author       = {Patrick Bahr and
                  Hans Bugge Grathwohl and
                  Rasmus Ejlers Møgelberg},
  title        = {The clocks are ticking: No more delays!},
  booktitle    = {{LICS} '17: 32nd Annual {ACM/IEEE} Symposium on
                  Logic in Computer Science, Reykjavík, Iceland,
                  June 20--23, 2017},
  pages        = {1--12},
  publisher    = {{IEEE} Computer Society},
  year         = {2017},
% url          = {https://doi.org/10.1109/LICS.2017.8005097},
  url          = {https://bahr.io/pubs/files/bahr17types-extended\%20abstract.pdf},
  doi          = {10.1109/LICS.2017.8005097},
}

@inproceedings{later_nakano,
  author       = {Hiroshi Nakano},
  title        = {A Modality for Recursion},
  booktitle    = {{LICS} 2000: 15th Annual {IEEE} Symposium on
                  Logic in Computer Science, Santa Barbara, California, USA,
                  June 26--29, 2000},
  pages        = {255--266},
  publisher    = {{IEEE} Computer Society},
  year         = {2000},
% url          = {https://doi.org/10.1109/LICS.2000.855774},
  url          = {https://www602.math.ryukoku.ac.jp/~nakano/papers/modality-lics00.pdf},
  doi          = {10.1109/LICS.2000.855774},
}

@misc{ornaments,
  author = {Conor {McBride}},
  title  = {Ornamental Algebras, Algebraic Ornaments},
  year   = {2011},
  url    = {https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/LitOrn.pdf},
}


% Misc type stuff {{{1

@inproceedings{local,
  author    = {Michael Vollmer and
               Chaitanya Koparkar and
               Mike Rainey and
               Laith Sakka and
               Milind Kulkarni and
               Ryan R. Newton},
  editor    = {Kathryn S. McKinley and
               Kathleen Fisher},
  title     = {{LoCal}: a language for programs operating on serialized data},
  booktitle = {Proceedings of the 40th {ACM} {SIGPLAN} Conference on Programming
               Language Design and Implementation, {PLDI} 2019, Phoenix, AZ,
               USA, June 22-26, 2019},
  pages     = {48--62},
  publisher = {{ACM}},
  year      = {2019},
  url       = {http://recurial.com/pldi19main.pdf},
  doi       = {10.1145/3314221.3314631},
}

@article{mlsub-pearl,
  author    = {Parreaux, Lionel},
  title     = {The simple essence of algebraic subtyping: principal type
               inference with subtyping made easy (functional pearl)},
  year      = {2020},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  volume    = {4},
  number    = {ICFP},
  url       = {https://doi.org/10.1145/3409006},
  doi       = {10.1145/3409006},
  journal   = {Proc. ACM Program. Lang.},
  month     = {aug},
}


% Misc implementation {{{1

@article{expl-sub,
  author    = {Martín Abadi and
               Luca Cardelli and
               Pierre{-}Louis Curien and
               Jean{-}Jacques Lévy},
  title     = {Explicit Substitutions},
  journal   = {J. Funct. Program.},
  volume    = {1},
  number    = {4},
  pages     = {375--416},
  year      = {1991},
% url       = {https://doi.org/10.1017/S0956796800000186},
  url       = {http://lucacardelli.name/Papers/ExplicitSub.pdf},
  doi       = {10.1017/S0956796800000186}
}

@article{modal-mltt,
  author       = {Gratzer, Daniel and Sterling, Jonathan and Birkedal, Lars},
  location     = {New York, NY, USA},
  publisher    = {ACM},
  date         = {2019-07},
  doi          = {10.1145/3341711},
  issn         = {2475-1421},
  journaltitle = {Proceedings of the {ACM} on Programming Languages},
  keywords     = {Modal types,dependent types,normalization by evaluation,type-checking},
  number       = {{ICFP}},
  pages        = {107:1--107:29},
  title        = {Implementing a Modal Dependent Type Theory},
  volume       = {3},
  url          = {https://www.jonmsterling.com/pdfs/modal-mltt.pdf},
  note         = {implementation at
                  \url{https://www.jonmsterling.com/resources/blott.tar.gz}}
}

@article{cbpv,
  author    = {Paul Blain Levy},
  title     = {Call-by-push-value: Decomposing call-by-value and call-by-name},
  journal   = {High. Order Symb. Comput.},
  volume    = {19},
  number    = {4},
  pages     = {377--414},
  year      = {2006},
  % url       = {https://doi.org/10.1007/s10990-006-0480-6},
  url       = {https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf},
  doi       = {10.1007/s10990-006-0480-6},
}

@article{defunc,
  author  = {Yulong Huang and Jeremy Yallop},
  title   = {Defunctionalization with Dependent Types},
  journal = {Proceedings of the {ACM} on Programming Languages},
  volume  = {7},
  number  = {{PLDI}},
  pages   = {516--538},
  year    = {2023},
  url     = {https://doi.org/10.1145/3591241},
  doi     = {10.1145/3591241},
}

@inproceedings{delcont-callcc,
  author       = {Martin Gasbichler and Michael Sperber},
  editor       = {Mitchell Wand and Simon L. Peyton Jones},
  title        = {Final shift for \texttt{call/cc}:
                  direct implementation of shift and reset},
  journaltitle = {Proceedings of the {ACM} on Programming Languages},
  number       = {{ICFP}},
  pages        = {271--282},
  publisher    = {{ACM}},
  year         = {2002},
  % url          = {https://doi.org/10.1145/581478.581504},
  url          = {https://www.cs.tufts.edu/~nr/cs257/archive/mike-sperber/shift-reset-direct.pdf},
  doi          = {10.1145/581478.581504},
}

% vim: set fdm=marker :