Mercurial > cpdt > repo
comparison src/Intro.v @ 350:ad315efc3b6b
Stub out new chapter
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 26 Oct 2011 11:19:52 -0400 |
parents | 4a432659a698 |
children | 3322367e955d |
comparison
equal
deleted
inserted
replaced
349:de7db21a016c | 350:ad315efc3b6b |
---|---|
73 (** | 73 (** |
74 A language with %\textit{%#<i>#dependent types#</i>#%}% may include references to programs inside of types. For instance, the type of an array might include a program expression giving the size of the array, making it possible to verify absence of out-of-bounds accesses statically. Dependent types can go even further than this, effectively capturing any correctness property in a type. For instance, later in this book, we will see how to give a Mini-ML compiler a type that guarantees that it maps well-typed source programs to well-typed target programs. | 74 A language with %\textit{%#<i>#dependent types#</i>#%}% may include references to programs inside of types. For instance, the type of an array might include a program expression giving the size of the array, making it possible to verify absence of out-of-bounds accesses statically. Dependent types can go even further than this, effectively capturing any correctness property in a type. For instance, later in this book, we will see how to give a Mini-ML compiler a type that guarantees that it maps well-typed source programs to well-typed target programs. |
75 | 75 |
76 %\index{ACL2}%ACL2 and %\index{HOL}%HOL lack dependent types outright. %\index{PVS}%PVS and %\index{Twelf}%Twelf each supports a different strict subset of Coq's dependent type language. Twelf's type language is restricted to a bare-bones, monomorphic lambda calculus, which places serious restrictions on how complicated %\textit{%#<i>#computations inside types#</i>#%}% can be. This restriction is important for the soundness argument behind Twelf's approach to representing and checking proofs. | 76 %\index{ACL2}%ACL2 and %\index{HOL}%HOL lack dependent types outright. %\index{PVS}%PVS and %\index{Twelf}%Twelf each supports a different strict subset of Coq's dependent type language. Twelf's type language is restricted to a bare-bones, monomorphic lambda calculus, which places serious restrictions on how complicated %\textit{%#<i>#computations inside types#</i>#%}% can be. This restriction is important for the soundness argument behind Twelf's approach to representing and checking proofs. |
77 | 77 |
78 In contrast, %\index{PVS}%PVS's dependent types are much more general, but they are squeezed inside the single mechanism of %\textit{%#<i>#subset types#</i>#%}%, where a normal type is refined by attaching a predicate over its elements. Each member of the subset type is an element of the base type that satisfies the predicate. Chapter 6 of this book introduces that style of programming in Coq, while the remaining chapters of Part II deal with features of dependent typing in Coq that go beyond what PVS supports. | 78 In contrast, %\index{PVS}%PVS's dependent types are much more general, but they are squeezed inside the single mechanism of %\textit{%#<i>#subset types#</i>#%}%, where a normal type is refined by attaching a predicate over its elements. Each member of the subset type is an element of the base type that satisfies the predicate. Chapter 7 of this book introduces that style of programming in Coq, while the remaining chapters of Part II deal with features of dependent typing in Coq that go beyond what PVS supports. |
79 | 79 |
80 Dependent types are not just useful because they help you express correctness properties in types. Dependent types also often let you write certified programs %\textit{%#<i>#without writing anything that looks like a proof#</i>#%}%. Even with subset types, which for many contexts can be used to express any relevant property with enough acrobatics, the human driving the proof assistant usually has to build some proofs explicitly. Writing formal proofs is hard, so we want to avoid it as far as possible, so dependent types are invaluable. | 80 Dependent types are not just useful because they help you express correctness properties in types. Dependent types also often let you write certified programs %\textit{%#<i>#without writing anything that looks like a proof#</i>#%}%. Even with subset types, which for many contexts can be used to express any relevant property with enough acrobatics, the human driving the proof assistant usually has to build some proofs explicitly. Writing formal proofs is hard, so we want to avoid it as far as possible, so dependent types are invaluable. |
81 | 81 |
82 *) | 82 *) |
83 | 83 |
223 \hline | 223 \hline |
224 Inductive Predicates & \texttt{Predicates.v} \\ | 224 Inductive Predicates & \texttt{Predicates.v} \\ |
225 \hline | 225 \hline |
226 Infinite Data and Proofs & \texttt{Coinductive.v} \\ | 226 Infinite Data and Proofs & \texttt{Coinductive.v} \\ |
227 \hline | 227 \hline |
228 General Recursion & \texttt{GeneralRec.v} \\ | |
229 \hline | |
228 Subset Types and Variations & \texttt{Subset.v} \\ | 230 Subset Types and Variations & \texttt{Subset.v} \\ |
229 \hline | 231 \hline |
230 More Dependent Types & \texttt{MoreDep.v} \\ | 232 More Dependent Types & \texttt{MoreDep.v} \\ |
231 \hline | 233 \hline |
232 Dependent Data Structures & \texttt{DataStruct.v} \\ | 234 Dependent Data Structures & \texttt{DataStruct.v} \\ |