CS304: Compilers

6.3: Functions of Semantic Analysis

• 6.3.1: Scope Checking of Names in a Program

  • Stanford University: Keith Schwarz's "Semantic Analysis" URL

    Read the notes and the slides for an overview of semantic analysis.

• 6.3.2: Static vs. Dynamic Scope Checking

  • University of California, Berkeley: Paul Hilfinger's "Static Semantics Overview" URL

    Read these slides.
    

• 6.3.3: Type Checking

  • Torben Ægidius Mogensen's "Basics of Compiler Design, Chapter 6: Type Checking" URL

    Read Chapter 6, which presents an overview of type checking, nicely organized: symbol table environment, type checking for expressions, functions, and then, for programs.

  • 6.3.3.1: Type Expressions, Type Equivalence, Type Inference, and What to Check

    • Massachusetts Institute of Technology: S. Amarasinghe and M. Rinard's "Semantic Analysis" URL

      Study the slides on type systems and what to check for when building intermediate representations for various language constructs.
      

    • University of California, Berkeley: Paul Hilfinger's "Types" URL

      Read slides 2 through 14 and use them as a review or supplement to the above readings. Slides 15 through 31 give examples of type inference for the languages Prolog, Java, and Python. 

    • University of California, Berkeley: Paul Hilfinger's "Lectures 18-21" Page

      These lectures correspond to the notes and are optional. They may be helpful in understanding some of the notes.

  • 6.3.3.2: Type Systems as Proof Systems-Type Checking as Proofs

    • Stanford University: Keith Schwarz's "Type Checking" URL

      Study the very interesting presentation on type checking by proofs.
      

    • University of California, Berkeley: Paul Hilfinger's "Type Inference and Unification" URL

      Read slides 1 through 8. The slides are somewhat formal and present a "type calculus." Use these slides to add to your understanding of types.
      

    • University of California, Berkeley: Paul Hilfinger's "Lecture 22" Page

      This video corresponds to these notes and is optional. If it adds to the notes and helps you, watch it.
      

  • 6.3.3.3: Applications of Type Proofs

    • Stanford University: Keith Schwarz's "Type Checking II" URL

      Study the application of the type proof system (introduced above) to the detection of type errors.

  • 6.3.3.4: Type Equations, Unification and Binding of Type Expressions

    • University of California, Berkeley: Paul Hilfinger's "Type Inference and Unification" URL

      Study slides 8 through 19. The slides supplement the readings above with type examples. A binding is a substitution of a type expression for a type variable.