I’m currently:
- 🔭 Doing research on semantics of programming languages, mathematics and logic for computation.
- 🌱 Teaching theory and practice of concurrency, quantum computing, and programming languages.
- 💻 Developing research and hobby projects such as:
- 🌀 rec-schemes: a Haskell library for recursion schemes, enabling elegant and compositional approaches to recursion and program structure.
- ⚙️ Markix: a minimalist operating system written from scratch in C and x86 assembly, used to explore low-level architecture, bootloaders, interrupts, and schedulers.
- 👯 Looking to collaborate on research connecting category theory, semantics, and computation.
- 🤔 Looking for help with doing OS development and connections with formal semantics
- 💬 Ask me about denotational semantics, lambda calculus, monads, or how interrupts and schedulers actually work at the hardware level.
- 📫 How to reach me: [email protected]
- ⚡ Fun fact: I switch between proof assistants and assembly debuggers with equal joy
A Haskell library implementing recursion schemes, providing elegant combinators for expressing recursive algorithms compositionally.
Inspired by category theory, this project explores how functors, algebras, and coalgebras capture recursion in a principled way.
⚙️ Markix
A minimalist operating system written in C and x86 assembly.
Markix boots from scratch, sets up the GDT, interrupts, and a round-robin scheduler, showing the structure of an OS from the ground up.
Aimed at educational and experimental exploration of protected mode, multitasking, and low-level OS internals.
⚙️ OSDev Notes
A TeX written notes to write an Intel x86 operating system from scratch written in C and x86 assembly.
- 📧 [email protected]
- 🧮 GitHub: @mpaviotti
- 🌐 Visit my website: mpaviotti.github.io