Shadows of Computation

JOIN NOW

Welcome to Shadows of Computation. This (free!) online course covers the foundations of category theory, which is used by computer scientists to abstract computing systems to reveal their intrinsic mathematical properties. This course is targeted towards those who are mathematically inclined, and interested in learning how category theory can be used in theoretical computer science.

There is also a secondary aim of the course: to teach how to present theoretical ideas. Two of the lectures will be about lecturing, and students will be encouraged to present a short talk at the end of the course, covering an extension of the ideas presented in the lectures.

This course will be taught at metauni, using Roblox for the 3D virtual environment and voice chat and Discord for community.

Time: starting October 10 2022, weekly 1.5 hour lectures on Mondays 19:30-21:00 AEDT (UTC +11), weekly 1 hour exercise sessions Wednesdays 20:00 AEDT (UTC +11). The class will run for 9 weeks. We realise that the timeslot will not be feasible in certain timezones, but this may not be a problem - see Asynchronous Attendance.
Location: Moonlight Forest, a 3D virtual world built in Roblox, which is part of metauni. At metauni we write on blackboards (which retain their contents when you leave) and talk using position-based voice chat (people far away can’t hear you). We also use the metauni Discord for communication outside of Roblox. See the instructions for how to set up spatial audio.

Important: you must have spatial voice set up (before you join a lecture) to hear other people speaking.

Goal: to introduce the beauty of category theory in a concrete way which reveals the philosophical ideas, the links to and between foundations, mathematics, and theoretical computer science. By concrete, we mean that we will not be telling you these ideas and insisting you accept them, but instead we will let the mathematics do the talking.
Resources: the textbook is the excellent textbook E. Rhiel “Category Theory in context”, which is available freely online. Other resources for the computer science component will be used and referenced throughout the course. An example of the ideas we will explore can be found here: “Theorems for free”.

Organisers:

Will Troiani (Fleetwood_Obdurate on Roblox) and Billy Snikkers (blinkybill on Roblox), neither with PhDs in category theory.

Course Schedule

Each lecture will be 1.5hr. In the schedule below, the references are given after the section number, eg R 1.3 refers to Section 1.3 of Category Theory in Context. The lecturer is given in brackets, (B) means Billy and (W) means Will (subject to change).

03-10-22 Welcome Introductions + Setup assistance.
10-10-22 Lecture 1: Making subtle ideas apparent (W) R 1.1 (notes, video, pocket).
24-10-22 Lecture 2: If it quacks like a duck… (B) R 1.3 (notes, video, pocket).
Lecture 3: Lecture 3: The gap between equivalent concepts (W) R 1.4 (The notes are spread out between this file and this file, video, pocket).
Lecture 4: A natural presentation (W) R 1.4 (notes, pocket).
Lecture 5: What is computation? (W) Lectures on the Curry-Howard Isomorphism, Gentzen-Mints-Zucker Duality, (notes, pocket).
Lecture 6: The line is part of a circle (W) R 2.2. (notes, pocket).
Lecture 7: Because it’s there (W) R 4.1, 5.1. (notes, pocket).
Lecture 8: Moggi’s Notions of Computation (W) Notions of Computation and Monads.

Exercise Sessions

We encourage learning by doing. Each week there will be assigned exercises for you to practice and better your understanding of the lecture content with your peers. There will be a regular exercise session on Wednesdays at 20:00 AEDT in Moonlight Forest, where you can get help from Billy, Will, or another experienced tutor.

It’s hard to pick a time that works for every timezone, so it is also encouraged for you to schedule your own times to meet with other students for a study/exercise session.

Exercise Sheets

Exercise sheets will appear here and also in the discord channels for each week.

Week 1: Exercises
Week 2: Exercises
Week 3: Exercises
Week 4: Exercises
Week 5: Exercises
Week 6: Exercises
Week 7: Exercises

Asynchronous Attendance

All lectures will be recorded and posted to the metauni youtube channel, but we will also experimenting with something we call replays. This means that we will present some lectures with VR, recording the presenters movements, writing and voice so that you can actually attend a past lecture in Roblox. Here’s our first attempt at it, which you can actually experience right now in The Rising Sea.

We think there’s some magic in replays, even beyond the ability to attend asynchronously, and we will run some replay viewing sessions where we’ll experiment with some of our ideas. Imagine being able to pause the replay-lecturer, and ask the real lecturer (or tutor) to clarify what was just said, or elaborate on some interesting tangent.

Registration

There’s a 45 student limit to the course, which is the most people we can have in a single Roblox server. So registration is essential for live attendance, but recorded lectures will be publicly available. Here is the registration process:

Follow Steps 1 and 2 of the instructions to setup your Roblox and Discord accounts.
Open the metauni Discord server and post in the #soc-registration channel with your Roblox username and how you want people to refer to you. This is mainly for your classmates, so you may wish to include a brief description of your interests and reasons for attending the class, and any links to personal webpages or Twitter accounts you want people to see. No pressure though, your Roblox username is enough (for administration purposes we need to know the connection between Discord accounts and Roblox usernames).
Join the metauni Roblox group. This way we can give you permission to write on the blackboards throughout metauni.
If you don’t check discord regularly, you can subscribe to the mailing list to receive important updates from now until the first class (this is the same mailing list used for mag). Otherwise you can watch the #shadows-of-computation channel in the metauni Discord for updates.

Pre-requisites

Only a little bit of linear algebra (a basic familiarity with finite dimensional complex vector spaces, for the sake of examples) is necessary. More precisely, you should have experience working with linear transformations and bases. You should know

The definition of a linear transformation,
The definition of a basis for a finite dimensional complex vector space.

We assume no familiarty nor experience with coding, computer science, or logic whatsoever.

You should also be comfortable with functions and terms like domain, codomain, injective, surjective, bijective, cartesian product.

For tablet and microphone recommendations see the hardware page.