PreTalent22.Overture
PreTalent22.Coq
- What is Coq?
- Why Coq?
- Curry-Howard correspondence
- Coq as a programming language and a logic
- Expressivity of Coq and pCuIC
PreTalent22.Arith
- Natural numbers
- Constructors
- Universes
- Recursive functions on inductive types (Fixpoints)
- Commutativity and associativity of addition
- Gauss
PreTalent22.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
PreTalent22.SplVM
- A stack-based virtual machine
- Stacks and stack elements
- VM instructions and programs
- A definitional interpreter for the VM
PreTalent22.Compiler
PreTalent22.Arith_in_class
- Natural numbers
- Constructors
- Universes
- Recursive functions on inductive types (Fixpoints)
- Commutativity and associativity of addition
- Gauss
PreTalent22.Spl_in_class
- 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
PreTalent22.Spl_completed
- 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
PreTalent22.SplVM_before_third_session
- A stack-based virtual machine
- Stacks and stack elements
- VM instructions and programs
- A definitional interpreter for the VM
PreTalent22.SplVM_in_class
- A stack-based virtual machine
- Stacks and stack elements
- VM instructions and programs
- A definitional interpreter for the VM