Mercurial > cpdt > repo

comparison src/Intro.v @ 350:ad315efc3b6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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} \\