# Types for Crash Preventionn

[Doktorsavhandling]

This thesis seeks to strengthen the capabilities of static polymorphic type-checking (as known from typed lambda calculus and functional programming) to allow a larger class of programming errors to be caught at compile time: the goal is to not only prevent illegal uses of data, but to also errors that lead to busy-loops, deadlocks, stack-overflows and heap-overflows.

The thesis exploits that, for recursive programs, many correctness properties (including freedom from errors leading to busy-loops, etc.) can be showed by induction. By the introduction of a *type-based induction principle* built-into the type inference rule for recursive functions, and by the definition of type systems to support its use, the desired strengthenings are achieved.

The method is limited to certain programming styles: it assumes the use of *recursive programming techniques*, and process interaction in *synchronous data-flow* style. The thesis explores these styles for *soft real-time embedded programming* - a field in which prevention of run-time crashes is an issue, and in which *type-based* crash-prevention techniques would complement the traditional techniques of the field, i.e., *formal methods* and *testing*.

The thesis contributes with *two experimental language designs* that each presents a strengthening of Milner and Damas's type-system: one higher-order, functional language with lazy semantics and implicit storage management, and in which well-typed programs dot not busy-loop, nor deadlock; one first-order, functional language with strict semantics and explicit storage management, and in which well-typed programs do not run out of stack-space, nor heap-space. It contributes with *two* *semantic theories* that are used to prove the correctness of the stronger type systems: one denotational theory in which crashing programs are viewed as `bottom', in which types excluding this value can be expressed, and in which recursive functions can be shown to be total mappings on such types by fix-point induction; one operational theory, in which a typed abstract machine is used to show that well-typed programs do not get stuck along a chain of reductions, and that a machine-configuration's stack and store never exceed bounds stated in its type. It contributes with a *type checking algorithm* for the first of the two type-systems.

**Nyckelord: **type systems, applicative (functional) programming (languages), concurrent programming, denotational semantics, data-flow, dynamic storage management, real-time systems and embedded systems, reliability, dependability

Denna post skapades 2006-08-25. Senast ändrad 2013-09-25.

CPL Pubid: 728