Types for Crash Preventionn

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. <p />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 <I>type-based induction principle</I> 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. <p />The method is limited to certain programming styles: it assumes the use of <I>recursive programming techniques</I>, and process interaction in <I>synchronous data-flow</I> style. The thesis explores these styles for <I>soft real-time embedded programming</I> - a field in which prevention of run-time crashes is an issue, and in which <I>type-based</I> crash-prevention techniques would complement the traditional techniques of the field, i.e., <I>formal methods</I> and <I>testing</I>. <p />The thesis contributes with <I>two experimental language designs</I> 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 <I>two</I> <I>semantic theories</I> 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 <I>type checking algorithm</I> for the first of the two type-systems