Embedding a logical theory of constructions in Agda

Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez. Embedding a logical theory of constructions in Agda. In Thorsten Altenkirch, Todd D. Millstein, editors, Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009. pages 59-66, ACM, 2009. [doi]

@inproceedings{BoveDS09,
  title = {Embedding a logical theory of constructions in Agda},
  author = {Ana Bove and Peter Dybjer and Andrés Sicard-Ramírez},
  year = {2009},
  doi = {10.1145/1481848.1481857},
  url = {http://doi.acm.org/10.1145/1481848.1481857},
  researchr = {https://researchr.org/publication/BoveDS09},
  cites = {0},
  citedby = {0},
  pages = {59-66},
  booktitle = {Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009},
  editor = {Thorsten Altenkirch and Todd D. Millstein},
  publisher = {ACM},
  isbn = {978-1-60558-330-3},
}