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:

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

To be continued…

Trinity 2025

To be continued…