Look at my Oxford coursework

Blog

·

February 16, 2025

·

by

Sergey Ichtchenko

One thing that I love about Oxford is that all of the (maths and CS) courses are freely accessible on the internet!

I thought I’d take part in the joy of free information by sharing my solutions to the take-home exam problems that I was graded on in the MSc in Mathematics and Foundations of Computer Science (MFoCS) programme here at Oxford.

Some context: there are three academic terms (Michaelmas, Hilary, Trinity) at the university. For my programme, you have to do a total of 5 courses during the first two terms, and the last one is reserved for writing your master’s thesis. Each course is graded by a take-home exam called a mini-project that is given to you at the beginning of the 6-week Christmas and Easter vacations, and you have around 4 weeks to complete all of the projects you have chosen to do during the term. These are then graded on a scale of 0-100, with the grade boundaries being:

The courses are also split into “Schedule 1” and “Schedule 2” courses, with the latter supposedly being harder, but that really depends on who you ask and which course you take.

Michaelmas 2024

Computer-Aided Formal Verification

There are a lot of systems in the world that need to be absolutely 100% safe and secure from any bugs or exploits (processors, aircraft avionics, self-driving cars, cryptographic algorithms, etc etc). Unfortunately, just testing these systems isn’t good enough, since you can never be fully sure whether you’ve tested everything - and trying to do this has gone very wrong many times throughout history. With formal verification, we can design a mathematical model of a computer program called an LTS or Kripke Structure and then design algorithms to write mathematical proofs that a system does what it’s supposed to do. If you’ve ever heard of the Halting Problem, you’ll know that this is actually impossible to do in general! But we find ways around this problem anyway since we’re cool like that :D

I liked this course a lot and will be writing my master’s dissertation on a related topic!

Bonus content: I hosted a session of Oxford Online Maths Club explaining the basics of formal verification with fun puzzles

Distributed Processes, Types, and Programming

This course’s two main pillars are pi-calculus and session types. The point of the course is to formally define communication between arbitrary processes and explore theoretical results like soundness/completeness, reducibility, and projectability of different processes and types. One cool bit of research that I saw being done in this area is using session types to formally specify the SMTP (email) protocol, which currently only has a specification in English (which is a problem since natural languages aren’t well-suited for talking about precise technical details to be used for protocol implementation).

Also, the professor said in her feedback that my submission was “the best LaTeXed report”, which is nice :)

Information Theory

This course covers three things: entropy & information, generating optimal codes for arbitrary random variables, and determining what codes to use when passing information through noisy channels. Overall quite a nice course with lots of theoretical and mathematical results, but also a good few implementation exercises (that I chose to do in APL). The mini-project came completely out of left field: the option I picked told us to explain, construct, and implement BCH codes, which are a code type we didn’t cover during the course. Which would be fine, but turns out that to do this you also need to self-study a fair bit of abstract algebra and Galois theory! Anyway, it ended up being fun and I’m quite happy with my implementation :)

Hilary 2025

I took multiple courses this term, but ended up having to drop most of them since we are only supposed to take three Schedule 1 courses and two Schedule 2 courses. And then the mini-project for my only Schedule 2 course (Automata, Logic, and Games) ended up being so brutal that most students, including me, dropped it… So I only ended up submitting one project this term. Luckily, MFoCS students are able to take one of two Schedule 2 courses in Trinity as well, so not all is lost!

Lambda Calculus and Types

Lambda Calculus is a mathematician’s way to program. It is horribly inefficient but it’s great at proving things related to what’s computable and what isn’t. It’s a very minimal way of expressing programs and quite beautiful especially if you look at it for the first time.

This was a fun little project. It seemed a little intimidating at first, but then I realised it was all just a big functional programming exam and it went smoothly from there. Surprisingly little theory actually, I wish there were more theoretical exercises related to the latter half of the course where we covered types etc etc. Also, I was expecting to get a higher grade since I was very satisfied with my construction of the DFA in Lambda Calculus, but I got a comment that my construction could have been more efficient and straightforward. I forgot about a simple way to do things and just went forward with defining lists of lists of lists… oh well, I’ll know for next time :p

Trinity 2025

The final, summery term of university. The final two courses offered are so-called “reading courses”, and while you do get a few lectures it’s mostly reading the textbook on your own. I chose applied category theory, since I had taken the regular category theory course in Hilary without submitting a project, so I thought it would be nice to do so now.

Applied Category Theory

Category theory is all about dots and lines. But it also isn’t, it’s an abstract way of defining what a function is. In fact, it’s so abstract and broad that it finds applications literally everywhere, even in computer science! However, as a result, the results you get in category theory are extremely beautiful but often also extremely mundane when applied to real situations. Nevertheless, you do get to say cool phrases like “Obviously, an idempotent morphism splits iff its presheaf of left-invariant morphisms with its action given by precomposition is representable!” to intimidate other people and mathematicians. So that’s cool.

This project was very confusing to me for the first few weeks, and then it finally clicked when I found the right sources. Funny how that works :D

Thesis

I am also currently writing a thesis, will post it here when it’s done.