-
Notifications
You must be signed in to change notification settings - Fork 4
/
chap-preface.tex
91 lines (77 loc) · 5.11 KB
/
chap-preface.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
\chapter*{Preface}
This book provides an introduction to mechanizing the meta-theory of programming languages. Mechanizing formal systems and proofs about them plays an increasingly important role in this area, and being literate in mechanizing formal systems and proofs about them has become essential for students and researchers in programming languages and type systems. More importantly, mechanizing programming language theory will provide a deeper understanding, allows easy exploration of variations and extensions, and provides immediate feedback.
This exposition is intended for a broad range of readers, from
advanced undergraduates to PhD students and researchers. It is
written as a companion to B. Pierce's book ``Types and Programming
Languages'' (TAPL) that provides an introduction to how to mechanize
the meta-theory of types and programming languages. While it is meant
to be read at the same time as TAPL, we provide enough context and
background that it should also be easily accessible to a reader who
has read TAPL in the past or already has basic knowledge of types and
programming languages. We give a roadmap in Fig.~\ref{fig:roadmap}. The material from the core covers about one semester's worth of material and has been used at McGill University for teaching the course ``Language-based security'', a course open to advanced undergraduates and beginning graduate students, and leaves room to either explore more in depth some mechanizations or explore extensions.
\begin{figure}
\centering
\begin{tabular}{p{8cm}|p{2.4cm}|p{3.25cm}}
Topic & TAPL & META \\
\hline
\textbf{Basics} & & \\\hline\hline
Preliminaries & CH~1, CH~2 & CH \ref{chap:basic}\\
Basic Arith. Terms, Types and Proofs & CH~3, CH~8 & \\
\hline
Encoding Basic Terms and Types & & CH \ref{sec:terms-basic}, CH \ref{sec:types-basic} \\
Encoding Basic Proofs as Functions & & CH \ref{chap:proofs-basic} \\
\hline \hline
\textbf{Intermediate} & & \\\hline \hline
Untyped Lambda-calculus & CH 5 & \\
Encoding Variables and Binders & & CH \ref{sec:debruijn}, CH \ref{sec:HOAS-var} \\
\hline
Typed Lambda-Calculus & CH 8, CH 9 & \\
Encoding Hypothetical Derivations, i.e. Derivations that depend on
Assumptions & & CH \ref{sec:HOAS-Assumptions}\\
Encoding Proofs about Closed Derivations & & CH \ref{chap:proofs-closed-derivations} \\
Encoding Proofs about Hypoth. Derivations & & CH \ref{chap:proofs-open-derivations} \\
\hline\hline
\textbf{Advanced} & & \\\hline \hline
Normalization & CH 12 & CH \ref{chap:normalization}\\
% Encoding Normalization Proofs & & CH \ref{chap:normalization} \\
\end{tabular}
\caption{Roadmap}
\label{fig:roadmap}
\end{figure}
There are also interesting further extensions to explore (Fig. \ref{fig:extensions}); for most of those only Beluga code exists at this point without a detailed explanation.
\begin{figure}
% \begin{center}
\begin{tabular}{p{9cm}|p{2.25cm}|p{2.75cm}}
Topic & TAPL & META \\
\hline
Nameless Representation (De Bruijn) & CH 6 & CH 4.1, CH 6.1 \\
References & CH 13 & Planned \\
Exceptions & CH 14 & Beluga Code \\
Subtyping & CH 15 & Planned \\
Recursive Type & CH 20 & Planned\\
Bounded Quantification & CH 26 & Beluga Code \\
\end{tabular}
% \end{center}
\caption{Extensions}
\label{fig:extensions}
\end{figure}
A key question when mechanizing formal systems and proofs is the choice of proof environment. Here we have chosen Beluga, a dependently typed programming and proof environment, as it directly supports key and common concepts that frequently arise when describing formal systems and derivations within them; in particular it provides infrastructure for modelling variable binders and their scope; it supports first-class contexts to abstract, manage, and manipulate a set of assumptions; it supports modelling derivations that depend on assumptions; and it has built-in first-class (simultaneous) substitutions. As such, it provides one of the most advanced infrastructures for such an endeavor. As we will show, the theory of programming languages does
not require a deep and complicated mathematical apparatus, but can be carried out in a concrete, intuitive, and computational way, when the right abstractions are provided.
% This allows hands-on experimentation w
\paragraph{Note to instructors}
If you intend to use this material for your own course, we would love to hear from you. We welcome all comments, questions, and suggestions.
\paragraph{Acknowledgements} The following people have helped shape
and develop the companion. Agata Murawska deserves thanks for
improving the structure and organization of this text and carefully
proof-reading parts. Nicolas Jeannerod described the translation from
small-step to big-step semantics in Section \ref{sec:small-to-big}. Francisco Ferreira wrote up the normalization
proof for the simply typed lambda calculus (Chapter
\ref{chap:normalization}) which was originally developed by
Andrew Cave. Finally, thanks goes to the undergraduate and graduate
students at McGill University who read earlier versions of this
manuscript and played with \beluga as part of the graduate course on
types and programming languages.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End: