Ernesto Copello, Alvaro Tasistro, Bruno Bianchi. Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda. In Fernando Magno Quintão Pereira, editor, Programming Languages - 18th Brazilian Symposium, SBLP 2014, Maceio, Brazil, October 2-3, 2014. Proceedings. Volume 8771 of Lecture Notes in Computer Science, pages 62-76, Springer, 2014.
Abstract is missing.