PreTalent24.Overture
PreTalent24.Coq
- What is Coq?
- Why Coq?
- Curry-Howard correspondence
- Coq as a programming language and a logic
- Expressivity of Coq and pCuIC
PreTalent24.Arith
- Natural numbers
- Constructors
- Universes
- Recursive functions on inductive types (Fixpoints)
- Commutativity and associativity of addition
- Gauss
PreTalent24.Spl
- SimPle Language (SPL)
- The semantics of SPL
- What goes wrong when we get an error in evaluating SPL programs?
- The eval function respects types
- Type soundness
PreTalent24.SplVM
- A stack-based virtual machine
- Stacks and stack elements
- VM instructions and programs
- A definitional interpreter for the VM