Contents for Programming Languages (A Foundational Approach)
CMSC 221/321 Fall 2011

* Lecture 1
Course Intro
  Why study PL?
  How to study PL?
  Math background
  Programming
Example - arithmetic expressions


* Lecture 2
First example language: SAE (Simple Arithmetic Expressions)
Program 1.1: SAE eval  (SAE-interp.sml)
Fig 1.1: SAE[BS] - Eval relation
Fig 1.1a: SAE[BS] - ⇓ evaluation relation
Inductive definition of expressions
Small-Step semantics
Fig 1.2: SAE[SS]
Fig 1.3: Example: 2 step derivation
Fig 1.4: Example: 3 step derivation
Induction over Derivations in SAE[SS]
Theorem 1.2 [Progress for SAE[SS])
Equivalence of Big-Step and Small-Step Evaluation
Appendix: Transition systems


* Lecture 3
Contectual reductions (SAE[CR])
Fig 1.5: Example: evaluate 2 + ((5 + 8) * 4) using CR
Fig 1.6: SAE[CR] - Contextual Reductions for SAE
Program 1.2: Contextual reduction
Abstract Machine (the CK machine)
Fig 1.7: SAE[CK] - CK-machine for SAE
Program 1.3: CK machine for SAE  (SAE-context-reduction.sml)
Equivalence of SAE[CR] and SAE[CK]


* Lecture 4
SAEL - expanding SAE with variables and let
Fig 2.1: abstract syntax of SAEL
Fig 2.2: SAEL[BSv] - "By-Value" big-step sematics for SAEL
Fig 2.3: SAEL[BSn] - "By-Name" big-step sematics for SAEL
Fig 2.4: SAEL[SSv] - "By-Value" small-step sematics for SAEL
Fig 2.5: SAEL[SSn] - "By-Name" small-step sematics for SAE
Efficiency comparison of by-value and by-name binding
Variable terminology: binding, bound, free, scope
Substitution
Free variable capture, change of bound variable (α-conversion)
Program 2.1 "by-value" big-step evaluator for SAEL (prog_2_1.sml)


* Lecture 5
Contextual reduction systems for SAEL (CRv and CRn)
Fig 2.6: SAEL[CRv] By-Value Contextual Reductions for SAEL
Fig 2.7: SAEL[CRn] By-Name Contextual Reductions for SAEL
CK machine for SAEL (SAEL[CKv])
Fig 2.8: SAEL[CKv] - CK-machine for SAEL Subst-by-Value
Fig 2.9: SAEL[CKn] - CK-machine for SAEL Subst-by-Name
Environments
Fig 2.10: SAEL[BSEv] - SAEL Big-Step binding-by-value semantics
    with environments
Fig 2.11: SAEL[BSEn]
Program 2.2. "by-value" environment passing evaluator for SAEL
Program 2.3. "by-name" environment passing evaluator for SAEL
Fig 2.12: SAEL[CEKv] - CEK-machine for SAEL with bind-by-value
Program 2.4. Implementation of SEAL[CEKv] machine
Fig 2.13: SAEL[CEKn] - CEK-machine for SAEL with bind-by-value


* Lecture 6 (Chapter 3)
3.1 Functions and Recursion (SEALF / Fun)
Fig 3.1: abstract syntax of SAELF
Fig 3.2: SAELF[BSv] - "By-Value" big-step sematics for SAELF
Fig 3.3: SAELF[BSn] - "By-Name" big-step sematics for SAELF
Fig 3.4: SAELF[SSv] - "Call-By-Value" small-step sematics for SAELF
Fig 3.5: SAELF[SSn] - "Call-By-Name" small-step sematics for SAELF
3.2 Type Errors
3.3 Relation with the Pure λ-Calculus
Fig 3.6: Small-step semantics of the λ-calculus
3.4 Fun: Recursive functions
Fig 3.7: abstract syntax of Fun
Fig 3.8: Fun[BSv] - "Call-By-Value" big-step sematics for Fun
Fig 3.9: Fun[BSn] - "Call-By-Name" big-step sematics for Fun
Fig 3.10: Fun[SSv] - "Call-By-Value" small-step sematics for Fun
Fig 3.11: Fun[SSn] - "Call-By-Name" small-step sematics for Fun
Y combinators, letrec
Programs:
   prog_3_1.sml (Fun[BSv])
   prog_3_1.sml (Fun[BSn])
   prog_3_1.sml (Fun[BSEv])
   prog_3_1.sml (Fun[BSE] with letrec)
3.5 A denotational view of recursive functions
  recursive functions as fixed-points


* Lecture 7 (Chapter 4)
Static Semantics
  A simple Static Semantics of Fun (closed expressions)
  judgement: Γ ⊦ e ok 
Fig 4.1: SEAL[ok] - Rules for relative closure judgements: Γ ⊦ e ok
Theorem 4.1 [Soundness of ok] (approximate)
Lemma 4.2 [Inversion of ok judgements]
Lemma 4.3 [Weakening]
Lemma 4.4 [Substitution]
Lemma 4.5 [Preservation]
Lemma 4.6 [Progress]
Theorem 4.7 [Soundness]

* Hw 4 (hw4_sol.txt)
4.3: CR reduction system for CVB Fun (Fun[CRv)
4.4: Define a CEK abstract machine for CBV Fun (Fun[CEKv])
4.5: SML implementation of Fun[CEKv] (hw_4_5.sml)


* Lecture 8
TFun -- adding types and typing to Fun

Fig 4.1: abstract syntax of TFun
Fig 4.2: abstract syntax of TFun (revised)
Fig 4.3: TFun[Typ] - Rules for the typing judgement Γ ⊦ e: τ
Fig 4.4: TFun value expressions
Fig 4.5: TFun[SSv] - CBV small-step sematics for TFun
Fig 4.6: TFun[SSn] - CBN small-step sematics for TFun
Program 4.1: Implementation of TFun[BSv] using substitution
Program 4.2: Implementation of TFun[BSv] using environments, with
   letrec declarations
Program 4.3: Implementation of TFun[BSv] using environments, with
   letrec and using abstractors


* Lecture 9
Type soundness for TFun (Preservation and Progress Lemmas)
Recursive functions in TFun

* Hw 5 (hw5_sol.txt)
5.1: Proof of Substitution Lemma for TFun (Lecture 8, Lemma 4.9)
5.2: Proof of Lemma 4.11 (Lecture 8), uniqueness of typing
5.3: Proof of part (5) of Inversion Lemma (Lemma 4.8, Lecture 8)
5.4: Proof of part (3) of Canonical Forms Lemma (Lemma 4.10, Lecture 8)


* Lecture 10
Adding *, +, μ, poly to TFun to get PTFun

Fig 5.1: PTFun "Concrete" Syntax
Fig 5.2: PTFun Abstract Syntax
Fig 5.3: PTFun values and environments
Fig 5.4: Eprim. Primitive env for PTFun[BSv]
Fig 5.5: PTFun[BSv] -- PTFun Big-Step, CBV, Env-based evaluation
Fig 5.6: PTFun value expressions (for PTFun[SSv])
Fig 5.7: PTFun[SSv] - CBV small-step sematics for PTFun
Fig 5.8: PTFun[typ]
Fig 5.9: Γ0 - type environment for primities

* Hw 6
6.1: Implement type checker for TFun[*,+]
6.2: Implement BSv evaluator for PTFun
  (polymorphism for extra credit)


* Hw 7 - complete implementation of full PTFun (ptfun.tgz)


* Lecture 11 (Chapter 6)
Mutable Storage:
  Adding state to TFun through the ref operator (updateable ref cells)
Fig 6.1: Abstract Syntax of TFun[*,+,Ref]
Fig 6.2: Typing Rules for TFun[*,+,Ref]
Fig 6.3: TFun[*,+,Ref][SSv] - Small-step CBV evaluation
Type Soundness
Theorem 6.1 [Preservation]
Theorem 6.2 [Progress]


* Objects (objects.sml)
Developing an object model in SML.


* Hw 8 (hw8_sol.txt) [2010 Final Exam]
8.1: CK machine for TFun(→,*)  (TFun(→,*)[CK])
8.2: (a) typing states of TFun(→,*)[CK] machine
     (b) Preservation Lemma for typed TFun(→,*)[CK] machine