### Skapa referens, olika format (klipp och klistra)

**Harvard**

Bove, A. (2004) *Formalising Bitonic Sort using Dependent Types*. Göteborg : Chalmers University of Technology

** BibTeX **

@techreport{

Bove2004,

author={Bove, Ana},

title={Formalising Bitonic Sort using Dependent Types},

abstract={ 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.
},

publisher={Chalmers University of Technology},

place={Göteborg},

year={2004},

keywords={bitonic sort, dependent types, type theory},

}

** RefWorks **

RT Report

SR Print

ID 3222

A1 Bove, Ana

T1 Formalising Bitonic Sort using Dependent Types

YR 2004

AB 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.

PB Chalmers University of Technology

LA eng

OL 30