Abstract
We present a full certification of merge sort in the language Agda. It features: termination warrant without explicit proof, no proof cost to ensure that the output is sorted, and a succinct proof that the output is a permutation of the input.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Altenkirch, T., McBride, C., McKinna, J.: Why dependent types matter (2005), http://www.e-pig.org/downloads/ydtm.pdf
Brady, E.: Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 552–593 (2013)
The coq proof assistant reference manual (2009)
Lindley, S., McBride, C.: Hasochism: The pleasure and pain of dependently typed haskell programming. SIGPLAN Not. 48(12), 81–92 (2013)
Norell, U.: Towards a practical programming language based on dependent type theory, Ph.D. thesis (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Copello, E., Tasistro, Á., Bianchi, B. (2014). Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda. In: Quintão Pereira, F.M. (eds) Programming Languages. SBLP 2014. Lecture Notes in Computer Science, vol 8771. Springer, Cham. https://doi.org/10.1007/978-3-319-11863-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-11863-5_5
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11862-8
Online ISBN: 978-3-319-11863-5
eBook Packages: Computer ScienceComputer Science (R0)