Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs

Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, Ulf Norell. Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs. In Nadia Polikarpova, editor, Haskell '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022. pages 108-122, ACM, 2022. [doi]

@inproceedings{CockxME0N22,
  title = {Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs},
  author = {Jesper Cockx and Orestis Melkonian and Lucas Escot and James Chapman and Ulf Norell},
  year = {2022},
  doi = {10.1145/3546189.3549920},
  url = {https://doi.org/10.1145/3546189.3549920},
  researchr = {https://researchr.org/publication/CockxME0N22},
  cites = {0},
  citedby = {0},
  pages = {108-122},
  booktitle = {Haskell '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022},
  editor = {Nadia Polikarpova},
  publisher = {ACM},
  isbn = {978-1-4503-9438-3},
}