Mercurial > urweb
changeset 1891:779c390382b9
Manual: add a pointer to background reading on inference rule notation
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 17 Nov 2013 07:54:59 -0500 |
| parents | abb0e95dcaa1 |
| children | 907a82a44f01 |
| files | doc/manual.tex |
| diffstat | 1 files changed, 5 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/doc/manual.tex Thu Nov 14 06:36:36 2013 -0500 +++ b/doc/manual.tex Sun Nov 17 07:54:59 2013 -0500 @@ -619,6 +619,11 @@ In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values. +The notations used here are the standard ones of programming language semantics. They are probably the most effective way to convey this information. At the same time, most Ur/Web users can probably get by \emph{without} knowing the contents of this section! If you're interested in diving into the details of Ur typing but are unfamiliar with ``inference rule notation,'' I recommend the following book: +\begin{quote} + Benjamin C. Pierce, \emph{Types and Programming Languages}, MIT Press, 2002. +\end{quote} + Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules. We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed. \begin{itemize} \item $\Gamma \vdash \kappa$ expresses kind well-formedness.