Programming in Martin-Löf's Type Theory: An IntroductionClarendon Press, 1990 - 221 頁 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 type theory, with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples. |
內容
Introduction | 1 |
Enumeration sets | 6 |
The identification of sets propositions and specifications | 11 |
著作權所有 | |
16 個其他區段未顯示
常見字詞
a₁ apply apply(ƒ arbitrary assumption b₁ basic set theory Bool C₁ canonical expressions cartesian product chapter colour(x combinatory logic component computation rule cons(x constructive mathematics context corresponding defined definitional equality derivation disjoint union E C(a El(A El(X elimination rule empty set enumeration sets equal canonical elements equal elements equal sets equality rule evaluated example explained expression of arity extensional equality family of sets formal formation rule gives Id(A II-introduction II(A intensional interpretation introduced introduction rule intuitionistic judgement forms justified know the judgement lazy evaluation List(A listrec(1 logic Martin-Löf means monomorphic natrec(a natural deduction natural numbers noncanonical notation premise primitive constant programming languages proof prop propositional function prove recursion saturated expression selector semantics set constructor set forming operations Set(A sin(y specification Stack subset theory substitution succ(x syntactical tree Tree(A true universal quantifier urec(A variable of arity well-order well-order set