view latex/cpdt.tex @ 323:3513d8b0531a

thide parsing-motivating definitions at start of Predicates
author Adam Chlipala <adam@chlipala.net>
date Tue, 20 Sep 2011 11:08:05 -0400
parents 4cb3ba8604bc
children 06d11a6363cd
line wrap: on
line source
\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}

Copyright Adam Chlipala 2008-2011.


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}
\include{MoreDep.v}
\include{DataStruct.v}
\include{Equality.v}
\include{Generic.v}
\include{Universes.v}
\include{Match.v}
\include{Reflection.v}
\include{Large.v}
\include{Firstorder.v}
\include{DeBruijn.v}
\include{Hoas.v}
\include{Interps.v}
\include{Extensional.v}
\include{Intensional.v}
\include{OpSem.v}

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

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

\end{document}