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

Functional Program Correctness Through Types

Nils Anders Danielsson (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Göteborg : Chalmers University of Technology, 2007. ISBN: 978-91-7385-034-6.- 130 s.
[Doktorsavhandling]

This thesis addresses the problem of avoiding errors in functional programs. The thesis has three parts, discussing different aspects of program correctness, with the unifying theme that types are an integral part of the methods used to establish correctness.

The first part validates a common, but not obviously correct, method for reasoning about functional programs. In this method, dubbed "fast and loose reasoning", programs written in a language with non-terminating functions are treated as if they were written in a total language. It is shown that fast and loose reasoning is sound when the programs are written in a given total subset of the language, and the resulting properties are translated back to the partial setting using certain partial equivalence relations which capture the concept of totality.

The second part discusses a method for ensuring that functions meet specified time bounds. The method is aimed at implementations of purely functional data structures, which often make essential use of lazy evaluation to ensure good time complexity in the presence of persistence. The associated complexity analyses are often complicated and hence error-prone, but by annotating the type of every function with its time complexity, using an annotated monad to combine time complexities of subexpressions, it is ensured that no details are forgotten.

The last part of the thesis is a case study in programming with strong invariants enforced by the type system. A dependently typed object language is represented in the meta language, which is also dependently typed, in such a way that it is impossible to form ill-typed terms. An interpreter is then implemented for the object language by using normalisation by evaluation. By virtue of the strong types used this implementation is a proof that every term has a normal form, and hence normalisation is proved. This also seems to be the first formal account of normalisation by evaluation for a dependently typed language.

Nyckelord: program correctness, total languages, partial languages, time complexity, lazy evaluation, dependent types, strong invariants, well-typed syntax, normalisation by evaluation



Denna post skapades 2007-11-06. Senast ändrad 2013-09-25.
CPL Pubid: 61161

 

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)

Ämnesområden

Datalogi

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:


Fast and Loose Reasoning is Morally Correct


A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family


Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures


Examination

Datum: 2007-12-05
Tid: 10:15
Lokal: Lecture room EF, ED&IT building, Rännvägen 6B, Chalmers
Opponent: Professor Martin Hofmann, Institut für Informatik, Ludwig-Maximilians-Universität München, Germany

Ingår i serie

Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie 2715


Technical report D - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University 37