Mercurial > hg > Papers > 2017 > atton-master
comparison paper/atton-master.tex @ 22:c748fb296673
Update introduction
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 22 Jan 2017 16:35:37 +0900 |
| parents | 4307454b56bb |
| children | 36ce493604fb |
comparison
equal
deleted
inserted
replaced
| 21:a47122d914ea | 22:c748fb296673 |
|---|---|
| 100 \input{introduction.tex} | 100 \input{introduction.tex} |
| 101 | 101 |
| 102 \input{cbc.tex} | 102 \input{cbc.tex} |
| 103 | 103 |
| 104 \chapter{ラムダ計算と型システム} | 104 \chapter{ラムダ計算と型システム} |
| 105 \label{chapter:type} | |
| 105 \section{型システムとは} | 106 \section{型システムとは} |
| 106 \section{型なしラムダ計算} | 107 \section{型なしラムダ計算} |
| 107 \section{単純型付きラムダ計算} | 108 \section{単純型付きラムダ計算} |
| 108 \section{部分型付け} | 109 \section{部分型付け} |
| 109 \section{部分型と Continuation based C} | 110 \section{部分型と Continuation based C} |
| 110 | 111 |
| 111 \chapter{証明支援系言語 Agda による証明手法} | 112 \chapter{証明支援系言語 Agda による証明手法} |
| 113 \label{chapter:agda} | |
| 112 \section{依存型を持つ証明支援系言語 Agda} | 114 \section{依存型を持つ証明支援系言語 Agda} |
| 113 \section{Natural Deduction} | 115 \section{Natural Deduction} |
| 114 \section{Curry-Howard Isomorphism} | 116 \section{Curry-Howard Isomorphism} |
| 115 \section{Reasoning} | 117 \section{Reasoning} |
| 116 | 118 |
| 117 \chapter{Agda における Continuation based C の表現} | 119 \chapter{Agda における Continuation based C の表現} |
| 120 \label{chapter:subtype} | |
| 118 \section{CodeSegment の定義} | 121 \section{CodeSegment の定義} |
| 119 \section{DataSegment の定義} | 122 \section{DataSegment の定義} |
| 120 \section{ノーマルレベル計算の実行} | 123 \section{ノーマルレベル計算の実行} |
| 121 \section{MetaCodeSegment の定義} | 124 \section{MetaCodeSegment の定義} |
| 122 \section{MetaDataSegment の定義} | 125 \section{MetaDataSegment の定義} |