Programming in Martin-Lof's Type Theory
Published on 1. June 1990
Book
Hardback
231 pages
978-0-19-853814-1 (ISBN)
Description
In recent years several formalisms for program construction have been introduced. One such formalism is the type theory developed by Per Martin-Lof. 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.
More details
Language
English
Place of publication
Oxford
United Kingdom
Publishing group
Oxford University Press
Target group
College/higher education
Professional and scholarly
Illustrations
bibliography
ISBN-13
978-0-19-853814-1 (9780198538141)
Copyright in bibliographic data is held by Nielsen Book Services Limited or its licensors: all rights reserved.
Schweitzer Classification
Content
Part 1 Polymorphic sets: the semantics of the judgement forms; general rules; enumeration sets; Cartesian product of a family of sets; equality sets; natural numbers; lists; cartesian product of two sets; disjoint union of two sets; disjoint union of a family of sets; the set of small sets (the first universe); well-orderings; general trees. Part 2 Subsets: subsets in the basic set theory; the subset theory. Part 3 Monomorphic sets: types defining sets in terms of types. Part 4 Examples: some small examples; program derivation; specification of abstract data types.