A Machine Verified Distributed Sorting Algorithm

Jørgen H. Andersen, Ed Harcourt, K.V.S. Prasad


We present a verification of a distributed sorting algorithm in ALF,
an implementation of Martin L¨of's type theory. The implementation
is expressed as a program in a prioritized version of CBS, (the Calculus of Broadcasting Systems) which we have implemented in ALF. The specification is expressed in terms of an ALF type which represents the set of all sorted lists and an HML (Hennesey-Milner Logic) formula which expresses that the sorting program will input any number of data until it hears a value triggering the program to begin outputting the data in a sorted fashion. We gain expressive power from the type theory by inheriting the language of data, state expressions, and propositions.

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v3i4.19967
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library