• Title: Programming in Martin-Lof's Type Theory: An Introduction
• Author(s) Bengt Nordstrom (Author), Kent Petersson (Author), Jan M. Smith (Author)
• Publisher: Oxford University Press; First Edition edition (July 19, 1990)
• Hardcover: 232 pages
• eBook: PDF and Postscript
• Language: English
• ISBN-10: 0198538146
• ISBN-13: 978-0198538141
• Share This:  

Book Description

Several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-Lof. Well suited as a theory for program construction, it makes possible the expression of 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.

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.

This book contains a thorough introduction to type theory, with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples.

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.

• N/A

• Amazon

• Functional Programming
• Computer Programming
• Theory of Programming Languages
• Mathematical Logic - Computability, Set Theory, Model Theory, Proof Theory, etc.
• Category Theory
• Compiler/Interpreter Design and Construction

• Programming in Martin-Lof's Type Theory: An Introduction (Bengt Nordstrom, et al)
• The Mirror Site (1) - PDF
• The Mirror Site (2) - PDF

• Proofs and Types (Jean-Yves Girard, et al.)

  Deals with the mathematical background of the application to computer science of aspects of logic on typed lambda calculus (namely the correspondence between propositions and types). Treats both the traditional logic and its applications to computer science.

• Type Theory and Functional Programming (Simon Thompson)

  This book explores the role of Martin-Lof's constructive type theory in computer programming. The main focus of the book is how the theory can be successfully applied in practice.

• The Implementation of Functional Programming Languages

  This book is about implementations, not languages, it will make no attempt to extol the virtues of functional languages or the functional programming style, assumes that the reader is familiar with functional programming.

• Categories, Types, and Structures (Andrea Asperti, et al)

  This book introduces category theory at a level appropriate for computer scientists and provides practical examples in the context of programming language design.

• Purely Functional Data Structures (Chris Okasaki)

  This book describes data structures from the point of view of functional languages, with examples, and presents design techniques that allow programmers to develop their own functional data structures. All source code is given in Standard ML and Haskell.

• Mostly Adequate Guide To Functional Programming

  This is a book on the functional paradigm in general. We'll use the world's most popular functional programming language: JavaScript. This makes it possible to practice and apply your acquired knowledge each day on real world programs.

• Functional Programming in Python (David Mertz)

  It describes ways to avoid Python's imperative-style flow control, the nuances of callable functions, how to work lazily with iterators, and the use of higher-order functions. He also lists several third-party Python libraries useful for functional programming.

• Category Theory for the Sciences (David I. Spivak)

  Using databases as an entry to Category Theory, this book explains category theory by examples, and shows that category theory can be useful outside of mathematics as a rigorous, flexible, and coherent modeling language throughout the sciences.

• Category Theory for Programmers (Bartosz Milewski)

  In this category theory for programmers, the author illustrates all major concepts using computer code. You are probably aware that functional languages are closer to math than the more popular imperative languages. They also offer more abstracting power.

• Category Theory for Computing Science (Michael Barr, et al.)

  This book is a textbook in basic category theory, written specifically to be read by people in computing science. It expounds the constructions we feel are basic to category theory in the context of examples and applications to computing science.

• An Invitation to Applied Category Theory: Seven Sketches

  Category theory is now a powerful tool in science, informatics, and industry. This book offers a self-contained tour of applied category theory. Each chapter follows a single thread motivated by a real-world application and discussed with category-theoretic tools.