Guarded Recursion in Agda via Sized Types

Niccolò Veltri, Niels van der Weide. Guarded Recursion in Agda via Sized Types. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany. Volume 131 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019. [doi]

@inproceedings{VeltriW19,
  title = {Guarded Recursion in Agda via Sized Types},
  author = {Niccolò Veltri and Niels van der Weide},
  year = {2019},
  doi = {10.4230/LIPIcs.FSCD.2019.32},
  url = {https://doi.org/10.4230/LIPIcs.FSCD.2019.32},
  researchr = {https://researchr.org/publication/VeltriW19},
  cites = {0},
  citedby = {0},
  booktitle = {4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany},
  editor = {Herman Geuvers},
  volume = {131},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-107-8},
}