adam@311: \documentclass[12pt]{report} adam@311: \usepackage[]{inputenc} adam@311: \usepackage[T1]{fontenc} adam@468: \usepackage{lmodern} adam@311: \usepackage{fullpage} adam@311: \usepackage{coqdoc} adam@311: \usepackage{amsmath,amssymb} adam@311: \usepackage{url} adam@311: \usepackage{makeidx,hyperref} adam@311: adam@479: \newcommand{\naive}[0]{na\"ive} adam@479: adam@311: \title{Certified Programming with Dependent Types} adam@311: \author{Adam Chlipala} adam@311: adam@311: \makeindex adam@311: adam@311: \begin{document} adam@311: adam@311: \maketitle adam@311: adam@311: \thispagestyle{empty} adam@311: \mbox{}\vfill adam@311: \begin{center} adam@311: adam@370: Copyright Adam Chlipala 2008-2012. adam@311: adam@311: adam@311: This work is licensed under a adam@311: Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adam@311: Unported License. adam@311: The license text is available at: adam@311: adam@311: \end{center} adam@311: adam@311: \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center} adam@311: adam@311: \phantomsection adam@311: \tableofcontents adam@311: adam@311: \include{Intro.v} adam@311: \include{StackMachine.v} adam@311: \include{InductiveTypes.v} adam@311: \include{Predicates.v} adam@311: \include{Coinductive.v} adam@353: \include{Subset.v} adam@350: \include{GeneralRec.v} adam@311: \include{MoreDep.v} adam@311: \include{DataStruct.v} adam@311: \include{Equality.v} adam@311: \include{Generic.v} adam@311: \include{Universes.v} adam@324: \include{LogicProg.v} adam@311: \include{Match.v} adam@311: \include{Reflection.v} adam@311: \include{Large.v} adam@381: \include{ProgLang.v} adam@383: \include{Conclusion.v} adam@311: adam@311: \clearpage adam@311: \addcontentsline{toc}{chapter}{Bibliography} adam@311: \bibliographystyle{plain} adam@311: \bibliography{cpdt} adam@311: adam@311: \clearpage adam@311: \addcontentsline{toc}{chapter}{Index} adam@311: \printindex adam@311: adam@311: \end{document}