Mercurial > cpdt > repo

comparison latex/cpdt.tex @ 311:4cb3ba8604bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through first half of StackMachine, along with some reorganization of the build process
author Adam Chlipala <adam@chlipala.net>
date Mon, 29 Aug 2011 15:31:06 -0400
parents
children 06d11a6363cd
comparison
equal deleted inserted replaced
310:cf67b7d6ceac 311:4cb3ba8604bc
1 \documentclass[12pt]{report}
2 \usepackage[]{inputenc}
3 \usepackage[T1]{fontenc}
4 \usepackage{fullpage}
5 \usepackage{coqdoc}
6 \usepackage{amsmath,amssymb}
7 \usepackage{url}
8 \usepackage{makeidx,hyperref}
9
10 \title{Certified Programming with Dependent Types}
11 \author{Adam Chlipala}
12
13 \makeindex
14
15 \begin{document}
16
17 \maketitle
18
19 \thispagestyle{empty}
20 \mbox{}\vfill
21 \begin{center}
22
23 Copyright Adam Chlipala 2008-2011.
24
25
26 This work is licensed under a
27 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
28 Unported License.
29 The license text is available at:
30
31 \end{center}
32
33 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}
34
35 \phantomsection
36 \tableofcontents
37
38 \include{Intro.v}
39 \include{StackMachine.v}
40 \include{InductiveTypes.v}
41 \include{Predicates.v}
42 \include{Coinductive.v}
43 \include{Subset.v}
44 \include{MoreDep.v}
45 \include{DataStruct.v}
46 \include{Equality.v}
47 \include{Generic.v}
48 \include{Universes.v}
49 \include{Match.v}
50 \include{Reflection.v}
51 \include{Large.v}
52 \include{Firstorder.v}
53 \include{DeBruijn.v}
54 \include{Hoas.v}
55 \include{Interps.v}
56 \include{Extensional.v}
57 \include{Intensional.v}
58 \include{OpSem.v}
59
60 \clearpage
61 \addcontentsline{toc}{chapter}{Bibliography}
62 \bibliographystyle{plain}
63 \bibliography{cpdt}
64
65 \clearpage
66 \addcontentsline{toc}{chapter}{Index}
67 \printindex
68
69 \end{document}