FreeComputerBooks.com
Links to Free Computer, Mathematics, Technical Books all over the World


 Title: Programming in MartinLof'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
 ISBN10: 0198538146
 ISBN13: 9780198538141
 Share This:
Book Description
Several formalisms for program construction have appeared. One such formalism is the type theory developed by Per MartinLof. 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 welltyped 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 MartinLöf's Constructive Mathematics and Computer Programming is that this book uses a uniform notation for expressions.
About the Authors N/A
 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 MartinLof's Type Theory: An Introduction (Bengt Nordstrom, et al)
 The Mirror Site (1)  PDF
 The Mirror Site (2)  PDF

Proofs and Types (JeanYves 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 MartinLof'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 imperativestyle flow control, the nuances of callable functions, how to work lazily with iterators, and the use of higherorder functions. He also lists several thirdparty 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 selfcontained tour of applied category theory. Each chapter follows a single thread motivated by a realworld application and discussed with categorytheoretic tools.
:






















