Pre-Talent Track 2022

• Session 1 (04.02.2022):
  • What is Coq?
  • Arithmetic in Coq [Developed in class]
• Session 2 (11.02.2022):
  • The Simple Language (SPL) [Developed in class]
  • The SPL Virtual Machine
• Session 3 (18.02.2022):
  • The completed version of the Simple Language (SPL)
  • The SPL Virtual Machine, now with a complete definition for runVMInstr. [Developed in class]
  • The Compiler from SPL to SPL Virtual Machine and its correctness [Developed in class]

Links

• Software Foundations: https://softwarefoundations.cis.upenn.edu/