Mercurial > cpdt > repo
comparison src/Intro.v @ 332:4a432659a698
Remove Part IV
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 03 Oct 2011 11:15:51 -0400 |
| parents | 06d11a6363cd |
| children | ad315efc3b6b |
comparison
equal
deleted
inserted
replaced
| 331:2eeb96aa0426 | 332:4a432659a698 |
|---|---|
| 135 (** * Prerequisites *) | 135 (** * Prerequisites *) |
| 136 | 136 |
| 137 (** | 137 (** |
| 138 I try to keep the required background knowledge to a minimum in this book. I will assume familiarity with the material from usual discrete math and logic courses taken by undergraduate computer science majors, and I will assume that readers have significant experience programming in one of the ML dialects, in Haskell, or in some other, closely related language. Experience with only dynamically typed functional languages might lead to befuddlement in some places, but a reader who has come to understand Scheme deeply will probably be fine. | 138 I try to keep the required background knowledge to a minimum in this book. I will assume familiarity with the material from usual discrete math and logic courses taken by undergraduate computer science majors, and I will assume that readers have significant experience programming in one of the ML dialects, in Haskell, or in some other, closely related language. Experience with only dynamically typed functional languages might lead to befuddlement in some places, but a reader who has come to understand Scheme deeply will probably be fine. |
| 139 | 139 |
| 140 Part IV of this manuscript is about formalizing programming languages and compilers. That part certainly depends on basic knowledge of formal type systems, operational semantics, and the theorems usually proved about such systems. As a reference on these topics, I recommend %\emph{%#<i>#Types and Programming Languages#</i>#%}~\cite{TAPL}%, by Benjamin C. Pierce. However, my current plan is to break Part IV into a separate, online-only document, since I expect the formalization interests of many readers of the book to lie outside of programming languages. I do often use examples from programming languages in the earlier parts of the book, but I have tried to design them to be comprehensible on the basis of ML or Haskell experience alone. | 140 My background is in programming languages, formal semantics, and program verification. I sometimes use examples from that domain, As a reference on these topics, I recommend %\emph{%#<i>#Types and Programming Languages#</i>#%}~\cite{TAPL}%, by Benjamin C. Pierce; however, I have tried to choose examples so that they may be understood without background in semantics. |
| 141 *) | 141 *) |
| 142 | 142 |
| 143 | 143 |
| 144 (** * Using This Book *) | 144 (** * Using This Book *) |
| 145 | 145 |
| 243 \hline | 243 \hline |
| 244 Proof by Reflection & \texttt{Reflection.v} \\ | 244 Proof by Reflection & \texttt{Reflection.v} \\ |
| 245 \hline | 245 \hline |
| 246 Proving in the Large & \texttt{Large.v} \\ | 246 Proving in the Large & \texttt{Large.v} \\ |
| 247 \hline | 247 \hline |
| 248 First-Order Abstract Syntax & \texttt{Firstorder.v} \\ | |
| 249 \hline | |
| 250 Dependent De Bruijn Indices & \texttt{DeBruijn.v} \\ | |
| 251 \hline | |
| 252 Higher-Order Abstract Syntax & \texttt{Hoas.v} \\ | |
| 253 \hline | |
| 254 Type-Theoretic Interpreters & \texttt{Interps.v} \\ | |
| 255 \hline | |
| 256 Extensional Transformations & \texttt{Extensional.v} \\ | |
| 257 \hline | |
| 258 Intensional Transformations & \texttt{Intensional.v} \\ | |
| 259 \hline | |
| 260 Higher-Order Operational Semantics & \texttt{OpSem.v} \\ | |
| 261 \hline | |
| 262 \end{tabular} \end{center} | 248 \end{tabular} \end{center} |
| 263 | 249 |
| 264 % *) | 250 % *) |