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