cpdt.tex 1.23 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
\documentclass[12pt]{report}
\usepackage[]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\usepackage{url}
\usepackage{makeidx,hyperref}

\title{Certified Programming with Dependent Types}
\author{Adam Chlipala}

\makeindex

\begin{document}

\maketitle

\thispagestyle{empty}
\mbox{}\vfill
\begin{center}

23
Copyright Adam Chlipala 2008-2012.
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43


This work is licensed under a
Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
Unported License.
The license text is available at:

\end{center}

\begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}

\phantomsection
\tableofcontents

\include{Intro.v}
\include{StackMachine.v}
\include{InductiveTypes.v}
\include{Predicates.v}
\include{Coinductive.v}
\include{Subset.v}
44
\include{GeneralRec.v}
45 46 47 48 49
\include{MoreDep.v}
\include{DataStruct.v}
\include{Equality.v}
\include{Generic.v}
\include{Universes.v}
Adam Chlipala's avatar
Adam Chlipala committed
50
\include{LogicProg.v}
51 52 53
\include{Match.v}
\include{Reflection.v}
\include{Large.v}
Adam Chlipala's avatar
Adam Chlipala committed
54
\include{ProgLang.v}
Adam Chlipala's avatar
Adam Chlipala committed
55
\include{Conclusion.v}
56 57 58 59 60 61 62 63 64 65 66

\clearpage
\addcontentsline{toc}{chapter}{Bibliography}
\bibliographystyle{plain}
\bibliography{cpdt}

\clearpage
\addcontentsline{toc}{chapter}{Index}
\printindex

\end{document}