%; -*-Bibtex-*- %% 2022 @inproceedings{gratzer:stratified-lob:2022, author = {Gratzer, Daniel and Birkedal, Lars}, title = {A Stratified Approach to {L\"{o}b} Induction}, url = {https://jozefg.github.io/papers/a-stratified-approach-to-lob-induction.pdf}, editor = {Felty, Amy}, location = {Dagstuhl, Germany}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, year = {2022}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = 228, doi = {10.4230/LIPIcs.FSCD.2022.3}, location = {Saarbr\"{u}cken, Germany}, } @inproceedings{gratzer:mtt-normalization:2022, author = {Gratzer, Daniel}, year = 2022, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, doi = {10.1145/3531130.3532398}, title = {Normalization for Multimodal Type Theory}, series = {LICS ’22}, url = {https://jozefg.github.io/papers/2022-normalization-for-multimodal-type-theory-short.pdf}, location = {Saarbr\"{u}cken, Germany}, } @article{sterling:2022, title = {{A Cubical Language for Bishop Sets}}, author = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer}, url = {https://lmcs.episciences.org/9264}, doi = {10.46298/lmcs-18(1:43)2022}, journal = {{Logical Methods in Computer Science}}, volume = {{Volume 18, Issue 1}}, year = 2022, month = Mar, } @article{gratzer:fitchtt:2022, author = {Gratzer, Daniel and Cavallo, Evan and Kavvos, G. A. and Guatto, Adrien and Birkedal, Lars}, title = {Modalities and Parametric Adjoints}, year = 2022, issue_date = {July 2022}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = 23, number = 3, issn = {1529-3785}, url = {https://doi.org/10.1145/3514241}, doi = {10.1145/3514241}, journal = {ACM Trans. Comput. Logic}, month = {apr}, articleno = 18, numpages = 29, } %% 2021 @Unpublished{gratzer:crisp-induction:2021, author = {Gratzer, Daniel}, title = {Crisp induction for intensional identity types}, note = {Available at \url{https://jozefg.github.io/papers/crisp-induction-for-intensional-identity-types.pdf}}, year = {2021}, } @Unpublished{gratzer:adjoint-modalities:2021, author = {Gratzer, Daniel}, title = {Self-adjoint modalities in {MTT}}, note = {Available at \url{https://jozefg.github.io/papers/self-adjoint-modalities-in-mtt.pdf}}, year = {2021}, } @unpublished{gratzer:mtt-normalization:2021, author = {Gratzer, Daniel}, title = {Normalization for multimodal type theory}, year = 2021, note = {Available at \url{https://arxiv.org/abs/2106.01414}}, } @unpublished{gratzer:fitchtt:2021, author = {Gratzer, Daniel and Cavallo, Evan and Kavvos, {G.A.} and Guatto, Adrien and Birkedal, Lars}, title = {Modalities and Parametric Adjoints}, note = {Available at \url{https://jozefg.github.io/papers/modalities-and-parametric-adjoints.pdf}}, year = 2021, } @article{gratzer:mtt-journal:2021, title = {{Multimodal Dependent Type Theory}}, author = {Daniel Gratzer and G. A. Kavvos and Andreas Nuyts and Lars Birkedal}, url = {https://lmcs.episciences.org/7713}, doi = {10.46298/lmcs-17(3:11)2021}, journal = {{Logical Methods in Computer Science}}, volume = {{Volume 17, Issue 3}}, year = 2021, month = Jul, } @inbook{spies:2021, author = {Spies, Simon and G\"{a}her, Lennard and Gratzer, Daniel and Tassarotti, Joseph and Krebbers, Robbert and Dreyer, Derek and Birkedal, Lars}, title = {Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic}, year = 2021, isbn = 9781450383912, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3453483.3454031}, booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation}, pages = {80–95}, numpages = 16 } %% 2020 @Unpublished{gratzer:mtt-tech-report:2020, author = {Gratzer, Daniel and Kavvos, G.A. and Nuyts, Andreas, and Birkedal, Lars}, title = {Type Theory \`a la Mode}, year = 2020, note = {Technical report accompanying ``Multimodal Dependent Type Theory''. Available at \url{https://jozefg.github.io/papers/type-theory-a-la-mode.pdf}}, } @inproceedings{gratzer:mtt-conf:2020, 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}, booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science}, pages = {492–506}, numpages = 15, location = {Saarbr\"{u}cken, Germany}, series = {LICS ’20} } @misc{sterling:2020, title = {A Cubical Language for Bishop Sets}, author = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer}, year = 2020, eprint = {2003.01491}, archivePrefix ={arXiv}, primaryClass = {cs.LO} } @misc{gratzer:lccc:2020, title = {Syntactic categories for dependent type theory: sketching and adequacy}, author = {Daniel Gratzer and Jonathan Sterling}, year = 2020, eprint = {2012.10783}, archivePrefix ={arXiv}, primaryClass = {cs.LO} } %% 2019 @article{bizjak:2019, author = {Bizjak, Ale\v{s} and Gratzer, Daniel and Krebbers, Robbert and Birkedal, Lars}, title = {Iron: Managing Obligations in Higher-order Concurrent Separation Logic}, journal = {Proc. ACM Program. Lang.}, issue_date = {January 2019}, volume = 3, number = {POPL}, month = jan, year = 2019, issn = {2475-1421}, pages = {65:1--65:30}, articleno = 65, numpages = 30, url = {http://doi.acm.org/10.1145/3290378}, doi = {10.1145/3290378}, keywords = {Separation logic, concurrency, resource management}, } @article{gratzer:2019, author = {Gratzer, Daniel and Sterling, Jonathan and Birkedal, Lars}, title = {Implementing a Modal Dependent Type Theory}, journal = {Proc. ACM Program. Lang.}, issue_date = {August 2019}, volume = 3, number = {ICFP}, month = jul, year = 2019, issn = {2475-1421}, pages = {107:1--107:29}, articleno = 107, numpages = 29, url = {http://doi.acm.org/10.1145/3341711}, doi = {10.1145/3341711}, acmid = 3341711, keywords = {Modal types, dependent types, normalization by evaluation, type-checking}, } @InProceedings{sterling:2019, author = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer}, title = {{Cubical Syntax for Reflection-Free Extensional Equality}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {31:1--31:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = 2019, volume = 131, editor = {Herman Geuvers}, URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10538}, URN = {urn:nbn:de:0030-drops-105387}, doi = {10.4230/LIPIcs.FSCD.2019.31}, annote = {Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity} } %% 2018 @Unpublished{gratzer:addendum-to-first-steps:2018, author = {Daniel Gratzer}, title = {An Addendum to Section 7 of ``First Steps in Synthetic Guarded Domain Theory''}, note = {Available at \url{https://jozefg.github.io/papers/an-addendum-to-first-steps.pdf}}, year = 2018, } %% 2017 @Unpublished{gratzer:concurrent-stacks:2017, author = {Gratzer, Daniel and H{\o}ier, Mathias and Bizjak, Ale{\v{s}} and Birkedal, Lars}, title = {Formalizing Concurrent Stacks With Helping: A Case Study In Iris}, note = {Available at \url{https://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf}}, year = 2017, } @Unpublished{gratzer:independence:2017, author = {Daniel Gratzer}, title = {On The Independence of the Continuum Hypothesis}, note = {Available at \url{https://jozefg.github.io/papers/on-the-independence.pdf}}, year = 2017, }