Strong Static Type Checking for Functional Common Lisp

This thesis presents a type system which supports the strong static type checking of programs developed in an applicative subset of the Common Lisp language. The Lisp subset is augmented with a guard construct for function definitions, which allows type restrictions to be placed on the arguments. Guards support the analysis and safe use of partial functions, like CAR, which are well-defined only for arguments of a certain type. A language of type descriptors characterizes the type domain. Descriptors are composed into function signatures which characterize the guard and which map various combinations of actual parameter types to possible result types. From a base of signatures for a small collection of primitive functions, the system infers signatures for newly submitted functions. The system includes a type inference algorithm which handles constructs beyond the constraints of ML-style systems. Most notable are the free use of CONS to construct objects of undeclared type and the use ..