Author Description

Constructive Type theory has been a topic of research interest to computer scientists, mathematicians, logicians and philosophers for a number of years. For computer scientists it provides a framework which brings together logic and programming languages in a most elegant and fertile program development and verification can proceed within a single system. Viewed in a different way, type theory is a functional programming language with some novel features, such as the totality of all its functions, its expressive type system allowing functions whose result type depends upon the value of its input, and sophisticated modules and abstract types whose interfaces can contain logical assertions as well as signature information. A third point of view emphasizes that programs (or functions) can be extracted from proofs in the logic.The book can be thought of as giving both a first and a second course in type theory. It begins with introductory material on logic and functional programming, and follow this by presenting the system of type theory itself, together with many examples. As well as this, this book goes further, looking at the system from a mathematical perspective, thus elucidating a number of its important properties. This book then takes a critical look at the profusion of suggestions in the literature about why and how type theory could be augmented. In doing this, this book is aiming at a moving target; it must be the case that further developments will have been made before the book reaches the press. Nonetheless, such an survey can give the reader a much more developed sense of the potential of type theory, as well as giving the background of what is to come.