pub.bib

@inproceedings{SIT,
  title = {A Simpler Encoding of Indexed Types},
  author = {Tesla Zhang},
  year = 2021,
  booktitle = {Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development},
  location = {Republic of Korea},
  publisher = {ACM},
  address = {New York, NY, USA},
  series = {TyDe '21},
  doi = {10.1145/3471875.3472991},
  isbn = {978-1-4503-8616-6},
  eprinttype = {arXiv},
  archiveprefix = {arXiv},
  eprint = {2103.15408},
  numpages = 9
}
@misc{ExactlyApplied,
  title = {Elegant elaboration with function invocation},
  author = {Tesla Zhang},
  year = 2021,
  eprinttype = {arXiv},
  archiveprefix = {arXiv},
  url = {https://arxiv.org/abs/2105.14840},
  eprint = {2105.14840},
}
@misc{Guest,
  title = {A tutorial on implementing De Morgan cubical type theory},
  author = {Tesla Zhang},
  year = 2022,
  eprinttype = {arXiv},
  archiveprefix = {arXiv},
  url = {https://arxiv.org/abs/2210.08232},
  eprint = {2210.08232},
}
@misc{ExtTyApp,
  title = {Three non-cubical applications of extension types},
  author = {Tesla Zhang},
  year = 2023,
  eprinttype = {arXiv},
  archiveprefix = {arXiv},
  url = {https://arxiv.org/abs/2311.05658},
  eprint = {2311.05658},
}
@misc{FordHelix,
  title = {Two tricks to trivialize higher-indexed families},
  author = {Tesla Zhang},
  year = 2023,
  eprinttype = {arXiv},
  archiveprefix = {arXiv},
  url = {https://arxiv.org/abs/2309.14187},
  eprint = {2309.14187},
}