Mercurial > cpdt > repo
annotate latex/cpdt.tex @ 569:0ce9829efa3b
Back to working in Coq 8.4
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 20 Jan 2019 15:28:23 -0500 |
| parents | dcb240e19167 |
| children |
| rev | line source |
|---|---|
| adam@311 | 1 \documentclass[12pt]{report} |
| adam@311 | 2 \usepackage[]{inputenc} |
| adam@311 | 3 \usepackage[T1]{fontenc} |
| adam@468 | 4 \usepackage{lmodern} |
| adam@311 | 5 \usepackage{fullpage} |
| adam@311 | 6 \usepackage{coqdoc} |
| adam@311 | 7 \usepackage{amsmath,amssymb} |
| adam@311 | 8 \usepackage{url} |
| adam@311 | 9 \usepackage{makeidx,hyperref} |
| adam@311 | 10 |
| adam@479 | 11 \newcommand{\naive}[0]{na\"ive} |
| adam@479 | 12 |
| adam@311 | 13 \title{Certified Programming with Dependent Types} |
| adam@311 | 14 \author{Adam Chlipala} |
| adam@311 | 15 |
| adam@311 | 16 \makeindex |
| adam@311 | 17 |
| adam@311 | 18 \begin{document} |
| adam@311 | 19 |
| adam@311 | 20 \maketitle |
| adam@311 | 21 |
| adam@532 | 22 A print version of this book is available from the MIT Press. For more information, see the book's home page: |
| adam@532 | 23 |
| adam@532 | 24 \begin{center} \url{http://adam.chlipala.net/cpdt/} \end{center} |
| adam@532 | 25 |
| adam@311 | 26 \thispagestyle{empty} |
| adam@311 | 27 \mbox{}\vfill |
| adam@311 | 28 \begin{center} |
| adam@311 | 29 |
| adam@551 | 30 Copyright Adam Chlipala 2008-2013, 2015, 2017. |
| adam@311 | 31 |
| adam@311 | 32 |
| adam@311 | 33 This work is licensed under a |
| adam@311 | 34 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
| adam@311 | 35 Unported License. |
| adam@311 | 36 The license text is available at: |
| adam@311 | 37 |
| adam@311 | 38 \end{center} |
| adam@311 | 39 |
| adam@311 | 40 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center} |
| adam@311 | 41 |
| adam@311 | 42 \phantomsection |
| adam@311 | 43 \tableofcontents |
| adam@311 | 44 |
| adam@311 | 45 \include{Intro.v} |
| adam@311 | 46 \include{StackMachine.v} |
| adam@311 | 47 \include{InductiveTypes.v} |
| adam@311 | 48 \include{Predicates.v} |
| adam@311 | 49 \include{Coinductive.v} |
| adam@353 | 50 \include{Subset.v} |
| adam@350 | 51 \include{GeneralRec.v} |
| adam@311 | 52 \include{MoreDep.v} |
| adam@311 | 53 \include{DataStruct.v} |
| adam@311 | 54 \include{Equality.v} |
| adam@311 | 55 \include{Generic.v} |
| adam@311 | 56 \include{Universes.v} |
| adam@324 | 57 \include{LogicProg.v} |
| adam@311 | 58 \include{Match.v} |
| adam@311 | 59 \include{Reflection.v} |
| adam@311 | 60 \include{Large.v} |
| adam@381 | 61 \include{ProgLang.v} |
| adam@383 | 62 \include{Conclusion.v} |
| adam@311 | 63 |
| adam@311 | 64 \clearpage |
| adam@311 | 65 \addcontentsline{toc}{chapter}{Bibliography} |
| adam@311 | 66 \bibliographystyle{plain} |
| adam@311 | 67 \bibliography{cpdt} |
| adam@311 | 68 |
| adam@311 | 69 \clearpage |
| adam@311 | 70 \addcontentsline{toc}{chapter}{Index} |
| adam@311 | 71 \printindex |
| adam@311 | 72 |
| adam@311 | 73 \end{document} |