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
  • Useful functions for working with results
  • The eval function
• 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
  • Useful functions for working with stack
• VM instructions and programs
• A definitional interpreter for the VM

PreTalent24.Compiler

• The compiler from SPL to SPLVM and its correctness
  • The result relation