Programming in Martin-Löf's Type Theory An Introduction |
|
| Author:
| Nordstrom, Bengt
Petersson, Kent
Smith, Jan M. |
| Series title: | International Series of Monographs on Computer Science |
| ISBN: | 978-0-19-853814-1 |
| Publication Date: | Jun 1990 |
| Publisher: | Oxford University Press, Incorporated
|
| Book Format: | Hardback |
| List Price: | AUD $105.00 |
Book Description:
|
In recent years, several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-Löf. 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. This book contains a thorough introduction to...
More DescriptionIn recent years, several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-Löf. 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. This book contains a thorough introduction to type theory, with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples.