|
adam@311
|
1 \documentclass[12pt]{report}
|
|
adam@311
|
2 \usepackage[]{inputenc}
|
|
adam@311
|
3 \usepackage[T1]{fontenc}
|
|
adam@468
|
4 \usepackage{lmodern}
|
|
adam@311
|
5 \usepackage{fullpage}
|
|
adam@311
|
6 \usepackage{coqdoc}
|
|
adam@311
|
7 \usepackage{amsmath,amssymb}
|
|
adam@311
|
8 \usepackage{url}
|
|
adam@311
|
9 \usepackage{makeidx,hyperref}
|
|
adam@311
|
10
|
|
adam@479
|
11 \newcommand{\naive}[0]{na\"ive}
|
|
adam@479
|
12
|
|
adam@311
|
13 \title{Certified Programming with Dependent Types}
|
|
adam@311
|
14 \author{Adam Chlipala}
|
|
adam@311
|
15
|
|
adam@311
|
16 \makeindex
|
|
adam@311
|
17
|
|
adam@311
|
18 \begin{document}
|
|
adam@311
|
19
|
|
adam@311
|
20 \maketitle
|
|
adam@311
|
21
|
|
adam@532
|
22 A print version of this book is available from the MIT Press. For more information, see the book's home page:
|
|
adam@532
|
23
|
|
adam@532
|
24 \begin{center} \url{http://adam.chlipala.net/cpdt/} \end{center}
|
|
adam@532
|
25
|
|
adam@311
|
26 \thispagestyle{empty}
|
|
adam@311
|
27 \mbox{}\vfill
|
|
adam@311
|
28 \begin{center}
|
|
adam@311
|
29
|
|
adam@536
|
30 Copyright Adam Chlipala 2008-2013, 2015.
|
|
adam@311
|
31
|
|
adam@311
|
32
|
|
adam@311
|
33 This work is licensed under a
|
|
adam@311
|
34 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
|
adam@311
|
35 Unported License.
|
|
adam@311
|
36 The license text is available at:
|
|
adam@311
|
37
|
|
adam@311
|
38 \end{center}
|
|
adam@311
|
39
|
|
adam@311
|
40 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}
|
|
adam@311
|
41
|
|
adam@311
|
42 \phantomsection
|
|
adam@311
|
43 \tableofcontents
|
|
adam@311
|
44
|
|
adam@311
|
45 \include{Intro.v}
|
|
adam@311
|
46 \include{StackMachine.v}
|
|
adam@311
|
47 \include{InductiveTypes.v}
|
|
adam@311
|
48 \include{Predicates.v}
|
|
adam@311
|
49 \include{Coinductive.v}
|
|
adam@353
|
50 \include{Subset.v}
|
|
adam@350
|
51 \include{GeneralRec.v}
|
|
adam@311
|
52 \include{MoreDep.v}
|
|
adam@311
|
53 \include{DataStruct.v}
|
|
adam@311
|
54 \include{Equality.v}
|
|
adam@311
|
55 \include{Generic.v}
|
|
adam@311
|
56 \include{Universes.v}
|
|
adam@324
|
57 \include{LogicProg.v}
|
|
adam@311
|
58 \include{Match.v}
|
|
adam@311
|
59 \include{Reflection.v}
|
|
adam@311
|
60 \include{Large.v}
|
|
adam@381
|
61 \include{ProgLang.v}
|
|
adam@383
|
62 \include{Conclusion.v}
|
|
adam@311
|
63
|
|
adam@311
|
64 \clearpage
|
|
adam@311
|
65 \addcontentsline{toc}{chapter}{Bibliography}
|
|
adam@311
|
66 \bibliographystyle{plain}
|
|
adam@311
|
67 \bibliography{cpdt}
|
|
adam@311
|
68
|
|
adam@311
|
69 \clearpage
|
|
adam@311
|
70 \addcontentsline{toc}{chapter}{Index}
|
|
adam@311
|
71 \printindex
|
|
adam@311
|
72
|
|
adam@311
|
73 \end{document}
|
