Programming Language Foundations (WSE)

<p>Preface 1</p>
<p>I Central Topics 7</p>
<p>1 Semantics of First–Order Arithmetic 9</p>
<p>1.1 Syntax of FO(Z) terms 10</p>
<p>1.2 Informal semantics of FO(Z) terms 10</p>
<p>1.3 Syntax of FO(Z) formulas 11</p>
<p>1.4 Some alternative logical languages for arithmetic 12</p>
<p>1.5 Informal semantics of FO(Z) formulas 13</p>
<p>1.6 Formal semantics of FO(Z) terms 14</p>
<p>1.6.1 Examples 17</p>
<p>1.7 Formal semantics of FO(Z) formulas 18</p>
<p>1.7.1 Examples 18</p>
<p>1.8 Compositionality 19</p>
<p>1.9 Validity and satisfiability 19</p>
<p>1.10 Interlude: proof by natural–number induction 20</p>
<p>1.11 Proof by structural induction 27</p>
<p>1.12 Conclusion 28</p>
<p>1.13 Basic exercises 29</p>
<p>1.14 Intermediate exercises 30</p>
<p>2 Denotational Semantics of WHILE 33</p>
<p>2.1 Syntax and informal semantics of WHILE 33</p>
<p>2.2 Beginning of the formal semantics for WHILE 34</p>
<p>2.3 Problem with the semantics of while–commands 35</p>
<p>2.4 Domains 37</p>
<p>2.5 Continuous functions 42</p>
<p>2.6 The least fixed–point theorem 46</p>
<p>2.7 Completing the formal semantics of commands 48</p>
<p>2.8 Connection to practice: static analysis using abstract interpretation 54</p>
<p>2.9 Conclusion 59</p>
<p>2.10 Basic exercises 60</p>
<p>2.11 Intermediate exercises 62</p>
<p>3 Axiomatic Semantics of WHILE 65</p>
<p>3.1 Denotational equivalence 66</p>
<p>3.2 Partial correctness assertions 68</p>
<p>3.3 Interlude: rules and derivations 71</p>
<p>3.4 Hoare Logic rules 76</p>
<p>3.5 Example derivations in Hoare Logic 82</p>
<p>3.6 Soundness of Hoare Logic and induction on the structure of derivations 87</p>
<p>3.7 Conclusion 92</p>
<p>3.8 Exercises 92</p>
<p>4 Operational Semantics of WHILE &nbsp;95</p>
<p>4.1 Big–step semantics of WHILE &nbsp;95</p>
<p>4.2 Small–step semantics of WHILE &nbsp;97</p>
<p>4.3 Relating the two operational semantics 101</p>
<p>4.4 Conclusion 120</p>
<p>4.5 Basic exercises 120</p>
<p>4.6 Intermediate exercises 122</p>
<p>5 Untyped Lambda Calculus 125</p>
<p>5.1 Abstract syntax of untyped lambda calculus 125</p>
<p>5.2 Operational semantics: full b–reduction 127</p>
<p>5.3 Defining full b–reduction with contexts 132</p>
<p>5.4 Specifying other reduction orders with contexts 134</p>
<p>5.5 Big–step call–by–value operational semantics 137</p>
<p>5.6 Relating big–step and small–step operational semantics 138</p>
<p>5.7 Conclusion 142</p>
<p>5.8 Basic Exercises 143</p>
<p>5.9 Intermediate Exercises 147</p>
<p>5.10 More Challenging Exercises 147</p>
<p>6 Programming in Untyped Lambda Calculus 149</p>
<p>6.1 The Church encoding for datatypes 149</p>
<p>6.2 The Scott encoding for datatypes 156</p>
<p>6.3 Other datatypes: lists 158</p>
<p>6.4 Non–recursive operations on Scott–encoded data 158</p>
<p>6.5 Recursive equations and the fix operator 160</p>
<p>6.6 Another recursive example: multiplication 162</p>
<p>6.7 Conclusion &nbsp;162</p>
<p>6.8 Basic exercises 163</p>
<p>6.9 Intermediate exercises 164</p>
<p>7 Simple Type Theory 167</p>
<p>7.1 Abstract syntax of simple type theory 167</p>
<p>7.2 Semantics of types 168</p>
<p>7.3 Type–assignment rules 169</p>
<p>7.4 Semantic soundness for type–assignment rules 169</p>
<p>7.5 Applying semantic soundness to prove normalization 171</p>
<p>7.6 Type preservation 173</p>
<p>7.7 The Curry–Howard isomorphism 176</p>
<p>7.8 Algorithmic typing 183</p>
<p>7.9 Algorithmic typing via constraint generation 186</p>
<p>7.10 Subtyping 190</p>
<p>7.11 Conclusion 199</p>
<p>7.12 Basic Exercises 200</p>
<p>7.13 Intermediate Exercises &nbsp;202</p>
<p>II Extra Topics 205</p>
<p>8 Nondeterminism and Concurrency 207</p>
<p>8.1 Guarded commands 207</p>
<p>8.2 Operational semantics of guarded commands 208</p>
<p>8.3 Concurrent WHILE 215</p>
<p>8.4 Operational semantics of concurrent WHILE &nbsp;216</p>
<p>8.5 Milner s Calculus of Communicating Systems 219</p>
<p>8.6 Operational semantics of CCS 220</p>
<p>8.7 Conclusion 226</p>
<p>8.8 Basic exercises 226</p>
<p>8.9 Intermediate exercises 228</p>
<p>9 More on Untyped Lambda Calculus 231</p>
<p>9.1 Confluence of untyped lambda calculus 231</p>
<p>9.2 Combinators 259</p>
<p>9.3 Conclusion 266</p>
<p>9.4 Basic exercises 266</p>
<p>9.5 Intermediate exercises 267</p>
<p>10 Polymorphic Type Theory 269</p>
<p>10.1 Type–assignment version of System F 269</p>
<p>10.2 Annotated terms for System F 271</p>
<p>10.3 Semantics of annotated System F 272</p>
<p>10.4 Programming with Church–encoded data 274</p>
<p>10.5 Higher–kind polymorphism and System Fw &nbsp;276</p>
<p>10.6 Conclusion 283</p>
<p>10.7 Exercises 283</p>
<p>11 Functional Programming 285</p>
<p>11.1 Call–by–value functional programming 286</p>
<p>11.2 Connection to practice: eager FP in OCaml</p>
<p>11.3 Lazy programming with call–by–name evaluation 300</p>
<p>11.4 Connection to practice: lazy FP in Haskell 304</p>
<p>11.5 Conclusion 310</p>
<p>11.6 Basic Exercises 310</p>
<p>11.7 Intermediate exercises 312</p>
<p>Mathematical Background 315</p>
<p>Bibliography 321</p>
<p>Index 325&nbsp;</p>