nLab Daniel Gratzer (changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

• personal page

Selected works

On categorical models of dependent types via locally Cartesian closed categories:

• Daniel Gratzer, Jonathan Sterling, Syntactic categories for dependent type theory: sketching and adequacy [[arXiv:2012.10783](https://arxiv.org/abs/2012.10783)]

On modal type theory:

• Daniel Gratzer, G. Alex Kavvos, Andreas Nuyts, Lars Birkedal: Multimodal Dependent Type Theory, Logical Methods in Computer Science 17 3 (2021) lmcs:7713 [[arXiv:2011.15021](https://arxiv.org/abs/2011.15021), doi:10.46298/lmcs-17(3:11)2021]

• Daniel Gratzer, Implementing Modal Dependent Type Theory, talk at ICFP 19 (slides pdf)

• Daniel Gratzer, Syntax and semantics of modal type theory, PhD Aarhus (2023) [[pdf](https://jozefg.github.io/papers/phd-thesis.pdf)]

On XTT:

• Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Cubical syntax for reflection-free extensional equality. In Herman Geuvers (ed.), 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:25. (arXiv:1904.08562, doi:10.4230/LIPIcs.FCSD.2019.31)

• Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, A Cubical Language for Bishop Sets, Logical Methods in Computer Science, 18 (1), 2022. (arXiv:2003.01491).