Inductive Invariants

Proofs: Numbers, Lists, Trees

Lambda Calculus

System F: Polymorphism

Abstract Syntax

Operational Semantics

Church Encodings

Compiler Correctness

Semantics via Interpreters

Hoare Logic

Simply Typed Lambda Calculus (STLC)

Simulation Relations

Functional Programming

Transition Systems

Metatheory

Type Safety in STLC

Graduel Types

CSE 505 Programming Languages University of Washington Spring 2021 University of Washington's course develops rigorous tools to study the meaning of programs. It aims to improve formalism, proof skills, and precision in programming, while also discussing practical applications. It covers operational semantics, Hoare Logic, compiler correctness, and more.  Develop tools to rigorously study what programs mean.

### Benefits

- Writing a PL-ish thing is inevitable
    - Extensible systems, rich data structures, domain-specific languages (DSLs)
- Build skills with formalism and proof
    - Precision, expressiveness, communication, clarity, confidence
- Become better programmers
    - Travel to understand where you’re from!


### Approach

- Develop the core of real languages
    - include distinguishing features, omit sugar
- Start simple, extend w/ richer features
    - develop reasoning techniques in parallel
- Discuss application to industrial PLs
    - implement and prove to connect theory with code

### Subgoals

- Develop tools for studying programs
    - structural induction, inference rules
- Investigate core PL concepts
    - types, functions, scope, mutation, iteration
- Learn how to use proof assistants
    - powerful tools with increasing adoption
  

CSE 505 Programming Languages

Programming Languages

Inductive Invariants

1 courses cover this concept

CSE 505 Programming Languages