CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Formalising Bitonic Sort using Dependent Types

Ana Bove (Institutionen för datavetenskap, Programmeringslogik)
Göteborg : Chalmers University of Technology, 2004.

We present a complete formalisation of bitonic sort and its correctness proof in constructive type theory. Bitonic sort is one of the fastest sorting algorithms where the sequence of comparisons is not data-dependent. In addition, it is a general recursive algorithm that works on sequences of length 2^n. In the formalisation we face two main problems: only structural recursion is allowed in type theory, and a formal proof of the correctness of the algorithm needs to consider quite a number of cases. We define the bitonic sort algorithm over dependently-typed binary trees with information in the leaves. In proving that the algorithm sorts its input we make use of the 0-1-principle. To support the use of that principle we also prove a parametricity theorem derived from the type of our bitonic sort from which the 0-1-principle can be proved.

Nyckelord: bitonic sort, dependent types, type theory

Denna post skapades 2006-08-25. Senast ändrad 2013-08-12.
CPL Pubid: 3222


Institutioner (Chalmers)

Institutionen för datavetenskap, Programmeringslogik (2002-2004)


Information Technology

Chalmers infrastruktur