Exercises

Lab 1: Introduction to ML

• Exercise 1: Getting Started with ML
• Exercise 2: Using ML with Emacs
• Exercise 3: Basic ML Programming

Lab 2: Introduction to HOL

• Exercise 4: Getting Started with HOL
• Exercise 5: Formalising CMOS in HOL
• Exercise 6: Proving the CMOS Not-Gate

Lab 3: Basic Proofs in HOL

• Exercise 7: First Proof Steps
• Exercise 8: Return to the CMOS Not-Gate

Lab 4: Arithmetic and Conversions

• Exercise 9: Conversions and Arithmetic

Lab 5: Timing

• Exercise 10: Timing

Lab 6: Replicated Components and Busses

• Exercise 11: The peANUt Logic Unit

Lab 7: Software Verification

• Exercise 12: Imperative Software Verification - A Deep Embedding

Lab 8: Hoare Logic

• Exercise 13: Hoare Logic