A series of notes on formal models and semantics.
These notes would not be possible without these amazing resources.
The notes draw heavily from these resources.
You can get the Coq files here: FMS Github
Content
- Lectures 1-4 give introduction to proofs and mechanization in Coq based off of Software Foundations.
- Lectures 5-7 formalize abstract machines in Coq (DFA and TM) based off of Regular Languages and Coq Library on Undecidability.
- Lectures 8-9 formalize IMP (imperative language) and axiomatic-semantics via Hoare logic based off of Software Foundations.
- Lectures 10-12 formalize Lambda Calculus, Simply-Typed Lambda Calculus (STLC), and Type-checking/Type Inference partially based off of Software Foundations.
- Lecture 13 goes over a proof of strong normalization of STLC via logical relations based off of Software Foundations.
Notes
- 01 - Introduction
- 02 - Functional Programming in Coq
- 03 - Proofs
- 04 - Inductive Propositions, Relations, and Curry-Howard
- 05 - Deterministic Finite Automata (DFA)
- 06 - Regular Expressions, NFAs, and DFAs
- 07 - Turing Machines and Decidability
- 08 - The IMP Language
- 09 - Hoare Logic and Axiomatic Semantics
- 10 - Lambda Calculus
- 11 - Simply-Typed Lambda Calculus
- 12 - Type Inference
- 13 - Normalization