I am delivering an Agda course for our 4th years.

I am co-delivering with Alasdair Lambert a digital logic, binary arithmetic, and assembly language course for 1st year students. I am focusing on the technology stack used during this course i.e. the Syrup programming language for circuit descriptions and testing, and the TINY machine based on a von Neumann architecture.

I am co-delivering with Bob Atkey a functional programming course for 3rd year students. Bob's original lecture notes are available online

I am delivering an Agda course for our 4th years.

I am delivering an Idris 2 course for SPLV 2023.

Documents

You can download the (WIP) SPLV lecture notes.

Day 1

• Slides Day 1
• Code (and corresponding package file as we need to tell Idris to not automatically load the prelude)

Day 2

• Slides Day 2
• Code (and accompanying library)

Day 3

• Slides Day 3
• Artefact for the Programming Over Serialised Data lecture