annotate latex/cpdt.tex @ 393:d40b05266306

Define 'certified program'
author Adam Chlipala <adam@chlipala.net>
date Sun, 22 Apr 2012 15:38:11 -0400
parents e2c88317611f
children 62475ab7570b
rev   line source
adam@311 1 \documentclass[12pt]{report}
adam@311 2 \usepackage[]{inputenc}
adam@311 3 \usepackage[T1]{fontenc}
adam@311 4 \usepackage{fullpage}
adam@311 5 \usepackage{coqdoc}
adam@311 6 \usepackage{amsmath,amssymb}
adam@311 7 \usepackage{url}
adam@311 8 \usepackage{makeidx,hyperref}
adam@311 9
adam@311 10 \title{Certified Programming with Dependent Types}
adam@311 11 \author{Adam Chlipala}
adam@311 12
adam@311 13 \makeindex
adam@311 14
adam@311 15 \begin{document}
adam@311 16
adam@311 17 \maketitle
adam@311 18
adam@311 19 \thispagestyle{empty}
adam@311 20 \mbox{}\vfill
adam@311 21 \begin{center}
adam@311 22
adam@370 23 Copyright Adam Chlipala 2008-2012.
adam@311 24
adam@311 25
adam@311 26 This work is licensed under a
adam@311 27 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adam@311 28 Unported License.
adam@311 29 The license text is available at:
adam@311 30
adam@311 31 \end{center}
adam@311 32
adam@311 33 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}
adam@311 34
adam@311 35 \phantomsection
adam@311 36 \tableofcontents
adam@311 37
adam@311 38 \include{Intro.v}
adam@311 39 \include{StackMachine.v}
adam@311 40 \include{InductiveTypes.v}
adam@311 41 \include{Predicates.v}
adam@311 42 \include{Coinductive.v}
adam@353 43 \include{Subset.v}
adam@350 44 \include{GeneralRec.v}
adam@311 45 \include{MoreDep.v}
adam@311 46 \include{DataStruct.v}
adam@311 47 \include{Equality.v}
adam@311 48 \include{Generic.v}
adam@311 49 \include{Universes.v}
adam@324 50 \include{LogicProg.v}
adam@311 51 \include{Match.v}
adam@311 52 \include{Reflection.v}
adam@311 53 \include{Large.v}
adam@381 54 \include{ProgLang.v}
adam@383 55 \include{Conclusion.v}
adam@311 56
adam@311 57 \clearpage
adam@311 58 \addcontentsline{toc}{chapter}{Bibliography}
adam@311 59 \bibliographystyle{plain}
adam@311 60 \bibliography{cpdt}
adam@311 61
adam@311 62 \clearpage
adam@311 63 \addcontentsline{toc}{chapter}{Index}
adam@311 64 \printindex
adam@311 65
adam@311 66 \end{document}