Programming in Martin-Löf's Type Theory: An Introduction

An introduction to type theory as a theory for program construction. Describes different type theories (theories of types, polymorphic and monomorphic sets, and subsets) from a computing science perspective.

**Tag(s):**
Functional Programming

**Publication date**: 31 Dec 1990

**ISBN-10**:
n/a

**ISBN-13**:
n/a

**Paperback**:
211 pages

**Views**: 15,326

Programming in Martin-Löf's Type Theory: An Introduction

An introduction to type theory as a theory for program construction. Describes different type theories (theories of types, polymorphic and monomorphic sets, and subsets) from a computing science perspective.

Terms and Conditions:

Book Excerpts:

Several formalisms for program construction have been introduced. One such formalism is the type theory developed by Per Martin-Löf. It is well suited as a theory for program construction since it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. This book contains an introduction to type theory as a theory for program construction.

As a programming language, type theory is similar to typed functional languages such as Hope and ML, but a major difference is that the evaluation of a well-typed program always terminates. In type theory it is also possible to write specifications of programming tasks as well as to develop provably correct programs. Type theory is therefore more than a programming language and it should not be compared with programming languages, but with formalized programming logics such as LCF and PL/CV.

One of the main differences between the type theory presentation in this book and the one in Per Martin-Löf's Constructive Mathematics and Computer Programming is that this book uses a uniform notation for expressions. Per Martin-Löf has formulated a theory of mathematical expressions in general, which is presented in chapter 3. This book describes how arbitrary mathematical expressions are formed and introduces an equality between expressions. This book also shows how defined constants can be introduced as abbreviations of more complicated expressions.

Intended Audience:

This book is intended for researchers and graduate students with an interest in the foundations of computing science, and it is mathematically self-contained.

Bengt Nordström wrote:This book was published by Oxford University Press in 1990. It is now out of print. This version is available from www.cs.chalmers.se/Cs/Research/Logic .

Book Excerpts:

Several formalisms for program construction have been introduced. One such formalism is the type theory developed by Per Martin-Löf. It is well suited as a theory for program construction since it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. This book contains an introduction to type theory as a theory for program construction.

As a programming language, type theory is similar to typed functional languages such as Hope and ML, but a major difference is that the evaluation of a well-typed program always terminates. In type theory it is also possible to write specifications of programming tasks as well as to develop provably correct programs. Type theory is therefore more than a programming language and it should not be compared with programming languages, but with formalized programming logics such as LCF and PL/CV.

One of the main differences between the type theory presentation in this book and the one in Per Martin-Löf's Constructive Mathematics and Computer Programming is that this book uses a uniform notation for expressions. Per Martin-Löf has formulated a theory of mathematical expressions in general, which is presented in chapter 3. This book describes how arbitrary mathematical expressions are formed and introduces an equality between expressions. This book also shows how defined constants can be introduced as abbreviations of more complicated expressions.

Intended Audience:

This book is intended for researchers and graduate students with an interest in the foundations of computing science, and it is mathematically self-contained.

Tweet

About The Author(s)

No information is available for this author.

No information is available for this author.

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