Mercurial > cpdt > repo

comparison src/Intro.v @ 491:da576746c3ba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix one reported grammatical error and make my own final pass over Chapter 1
author Adam Chlipala <adam@chlipala.net>
date Fri, 18 Jan 2013 13:45:00 -0500
parents a95af5a59990
children 6b3fb6672cfa
comparison
equal deleted inserted replaced
490:c8a3cb24bae9 491:da576746c3ba
73 73
74 74
75 (** ** Dependent Types *) 75 (** ** Dependent Types *)
76 76
77 (** 77 (**
78 A language with _dependent types_ 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. 78 A language with _dependent types_ 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 compiler a type that guarantees that it maps well-typed source programs to well-typed target programs.
79 79
80 %\index{ACL2}%ACL2 and %\index{HOL}%HOL lack dependent types outright. Each of %\index{PVS}%PVS and %\index{Twelf}%Twelf 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 _computations inside types_ can be. This restriction is important for the soundness argument behind Twelf's approach to representing and checking proofs. 80 %\index{ACL2}%ACL2 and %\index{HOL}%HOL lack dependent types outright. Each of %\index{PVS}%PVS and %\index{Twelf}%Twelf 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 _computations inside types_ can be. This restriction is important for the soundness argument behind Twelf's approach to representing and checking proofs.
81 81
82 In contrast, %\index{PVS}%PVS's dependent types are much more general, but they are squeezed inside the single mechanism of _subset types_, 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. 82 In contrast, %\index{PVS}%PVS's dependent types are much more general, but they are squeezed inside the single mechanism of _subset types_, 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.
83 83
186 (** ** Installation and Emacs Set-Up *) 186 (** ** Installation and Emacs Set-Up *)
187 187
188 (** 188 (**
189 At the start of the next chapter, I assume that you have installed Coq and Proof General. The code in this book is tested with Coq versions 8.4 and 8.4pl1. Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions. 189 At the start of the next chapter, I assume that you have installed Coq and Proof General. The code in this book is tested with Coq versions 8.4 and 8.4pl1. Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions.
190 190
191 %\index{Proof General|(}%To set up your Proof General environment to process the source to this chapter, a few simple steps are required. 191 %\index{Proof General|(}%To set up your Proof General environment to process the source to the next chapter, a few simple steps are required.
192 192
193 %\begin{enumerate}%#<ol># 193 %\begin{enumerate}%#<ol>#
194 194
195 %\item %#<li>#Get the book source from 195 %\item %#<li>#Get the book source from
196 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.tgz}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.tgz">http://adam.chlipala.net/cpdt/cpdt.tgz</a></tt></blockquote></li># 196 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.tgz}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.tgz">http://adam.chlipala.net/cpdt/cpdt.tgz</a></tt></blockquote></li>#
197 197
198 %\item %#<li>#Unpack the tarball to some directory <<DIR>>.#</li># 198 %\item %#<li>#Unpack the tarball to some directory <<DIR>>.#</li>#
199 199
200 %\item %#<li>#Run <<make>> in <<DIR>>.#</li># 200 %\item %#<li>#Run <<make>> in <<DIR>> (ideally with a <<-j>> flag to use multiple processor cores, if you have them).#</li>#
201 201
202 %\item %#<li>#There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the <<coqtop>> program, which provides the interactive Coq toplevel. One way to add settings that will be shared by many source files is to add a custom variable setting to your %\index{.emacs file@\texttt{.emacs} file}%<<.emacs>> file, like this: 202 %\item %#<li>#There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the <<coqtop>> program, which provides the interactive Coq toplevel. One way to add settings that will be shared by many source files is to add a custom variable setting to your %\index{.emacs file@\texttt{.emacs} file}%<<.emacs>> file, like this:
203 << 203 <<
204 (custom-set-variables 204 (custom-set-variables
205 ... 205 ...