Type Theory and Functional Programming

This book gives the formal system for type theory, developing examples of both programs and proofs. From the functional programming point of view, this book stresses the differences between the system and more traditional languages.

**Tag(s):**
Functional Programming

**Publication date**: 31 Dec 1991

**ISBN-10**:
0201416670

**ISBN-13**:
n/a

**Paperback**:
388 pages

**Views**: 16,654

Type Theory and Functional Programming

This book gives the formal system for type theory, developing examples of both programs and proofs. From the functional programming point of view, this book stresses the differences between the system and more traditional languages.

Book Excerpts:

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 way: 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.

Book Structure:

The first three chapters survey the three fields upon which type theory depends: logic, the lambda-calculus and functional programming and constructive mathematics. The surveys are short, establishing terminology, notation and a general context for the discussion; pointers to the relevant literature and in particular to more detailed introductions are provided. In the second chapter this book discusses some issues in the lambda-calculus and functional programming which suggest analogous questions in type theory.

The fourth chapter forms the focus of the book. This book gives the formal system for type theory, developing examples of both programs and proofs as we go along. These tend to be short, illustrating the construct just introduced - Chapter 6 contains many more examples.

The system is expressive, as witnessed by the previous chapter, but are programs given in their most natural or efficient form? Chapter 7 provides a host of proposals of how to augment the system.

Chapter eight examines the foundations of the system: how it compares with other systems for constructive mathematics, how models of it are formed and used and how certain of the rules, the closure rules, may be seen as being generated from the introduction rules, which state what are the canonical members of each type. The book ends with a survey of related systems, implemented or not, and some concluding remarks.

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 way: 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.

Book Structure:

The first three chapters survey the three fields upon which type theory depends: logic, the lambda-calculus and functional programming and constructive mathematics. The surveys are short, establishing terminology, notation and a general context for the discussion; pointers to the relevant literature and in particular to more detailed introductions are provided. In the second chapter this book discusses some issues in the lambda-calculus and functional programming which suggest analogous questions in type theory.

The fourth chapter forms the focus of the book. This book gives the formal system for type theory, developing examples of both programs and proofs as we go along. These tend to be short, illustrating the construct just introduced - Chapter 6 contains many more examples.

The system is expressive, as witnessed by the previous chapter, but are programs given in their most natural or efficient form? Chapter 7 provides a host of proposals of how to augment the system.

Chapter eight examines the foundations of the system: how it compares with other systems for constructive mathematics, how models of it are formed and used and how certain of the rules, the closure rules, may be seen as being generated from the introduction rules, which state what are the canonical members of each type. The book ends with a survey of related systems, implemented or not, and some concluding remarks.

Tweet

About The Author(s)

No information is available for this author.

Book Categories

Computer Science
Introduction to Computer Science
Introduction to Computer Programming
Algorithms and Data Structures
Artificial Intelligence
Computer Vision
Machine Learning
Neural Networks
Game Development and Multimedia
Data Communication and Networks
Coding Theory
Computer Security
Information Security
Cryptography
Information Theory
Computer Organization and Architecture
Operating Systems
Image Processing
Parallel Computing
Concurrent Programming
Relational Database
Document-oriented Database
Data Mining
Big Data
Data Science
Digital Libraries
Compiler Design and Construction
Functional Programming
Logic Programming
Object Oriented Programming
Formal Methods
Software Engineering
Agile Software Development
Information Systems
Geographic Information System (GIS)

Mathematics
Mathematics
Algebra
Abstract Algebra
Linear Algebra
Number Theory
Numerical Methods
Precalculus
Calculus
Differential Equations
Category Theory
Proofs
Discrete Mathematics
Theory of Computation
Graph Theory
Real Analysis
Complex Analysis
Probability
Statistics
Game Theory
Queueing Theory
Operations Research
Computer Aided Mathematics

Supporting Fields
Web Design and Development
Mobile App Design and Development
System Administration
Cloud Computing
Electric Circuits
Embedded System
Signal Processing
Integration and Automation
Network Science
Project Management

Operating System
Programming/Scripting
Ada
Assembly
C / C++
Common Lisp
Forth
Java
JavaScript
Lua
Microsoft .NET
Rexx
Perl
PHP
Python
R
Rebol
Ruby
Scheme
Tcl/Tk

Miscellaneous
Sponsors