Mercurial > cpdt > repo
annotate latex/cpdt.tex @ 318:70e51e8cfce7
New InductiveTypes exercises and difficulty markings
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 12 Sep 2011 16:42:51 -0400 |
| parents | 4cb3ba8604bc |
| children | 06d11a6363cd |
| 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@311 | 23 Copyright Adam Chlipala 2008-2011. |
| 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@311 | 43 \include{Subset.v} |
| adam@311 | 44 \include{MoreDep.v} |
| adam@311 | 45 \include{DataStruct.v} |
| adam@311 | 46 \include{Equality.v} |
| adam@311 | 47 \include{Generic.v} |
| adam@311 | 48 \include{Universes.v} |
| adam@311 | 49 \include{Match.v} |
| adam@311 | 50 \include{Reflection.v} |
| adam@311 | 51 \include{Large.v} |
| adam@311 | 52 \include{Firstorder.v} |
| adam@311 | 53 \include{DeBruijn.v} |
| adam@311 | 54 \include{Hoas.v} |
| adam@311 | 55 \include{Interps.v} |
| adam@311 | 56 \include{Extensional.v} |
| adam@311 | 57 \include{Intensional.v} |
| adam@311 | 58 \include{OpSem.v} |
| adam@311 | 59 |
| adam@311 | 60 \clearpage |
| adam@311 | 61 \addcontentsline{toc}{chapter}{Bibliography} |
| adam@311 | 62 \bibliographystyle{plain} |
| adam@311 | 63 \bibliography{cpdt} |
| adam@311 | 64 |
| adam@311 | 65 \clearpage |
| adam@311 | 66 \addcontentsline{toc}{chapter}{Index} |
| adam@311 | 67 \printindex |
| adam@311 | 68 |
| adam@311 | 69 \end{document} |