Mercurial > cpdt > repo
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} |