2014 | OriginalPaper | Buchkapitel
Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda
verfasst von : Ernesto Copello, Álvaro Tasistro, Bruno Bianchi
Erschienen in: Programming Languages
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.