Mikhail Ushakov

Profile

I am a software developer and MSc Software Science student at Radboud University Nijmegen. My academic interests include Term Rewriting, Functional Programming, and Compiler Construction. In software development, I am primarily interested in developing Java applications and Spring Boot APIs. Additionally, I have experience in IDE plugin development, physics simulation, computer graphics, data science, and competitive programming. I also actively used the following programming languages and technologies in my coursework and personal projects: Python, Haskell/Clean, OCaml, Rocq, C/C++, and MySQL.

Experience

Student Assistant

Radboud University Sep 2025 - Present

Student Assistant for the Data Mining and Machine Learning course

Technologies Used: Data Mining, Python, Jupyter, Machine Learning

Student Assistant

Radboud University Sep 2024 - Jan 2025

Student Assistant for the Data Mining and Machine Learning course

Technologies Used: Data Mining, Python, Jupyter, Machine Learning

Student Assistant

Radboud University Sep 2024 - Nov 2024

Student assistant for the Semantics and Correctness course

Technologies Used: While, Natural Semantics, Hoare Logic

Backend Developer

GiPHouse Feb 2024 - Jun 2024

I was working on the "Date A Tree" (ex. Tree Tinder) project developed for the Radboud UMC.
https://dateatree.com/
https://www.ru.nl/en/about-us/news/date-a-tree-connect-with-a-tree-to-connect-with-nature

Technologies Used: Kotlin, Python, Spring Boot, PostgreSQL, Flask

Student Assistant

Radboud University Jan 2024 - Apr 2025

Student assistant for the Semantics and Correctness course

Technologies Used: While, Natural Semantics, Hoare Logic

Student Assistant

Radboud University Sep 2023 - Jan 2024

Student assistant for the Data Mining course

Technologies Used: Data Mining, Python, Jupyter

Projects

WPP2TRS - Java library that allows translating While++ programs into the LCTRS

SPLCompiler - Simple Programming Language (SPL) compiler to the Simple Stack Machine (SSM)

DerivationTreeBuilder - Automatic generation of the derivation proof trees for While programs

CubeSolver - Rubik's cube solver written in pure C++ with OpenGL 3d visualization.

isabelle_x86asm - Isabelle x86 assembly formalization

LensRayTracing - Ray tracing and rays trajectory modeling for the cylindrical lens and single light source.

MinPropLogicProver - Small LCF-style prover for minimal propositional logic

IDE-News - The IntelliJ platform plugin that allows you to subscribe to different RSS channels and read your favorite news not leaving the IDE.

SingnalProcessor - The oscilloscope simulator that allows generating and visualizing different signals. Also, it is possible to add noise to the signals and then analyze and transform them.

PGMpp - The image manipulation library for PGM images format.

ElectricField - The interactive physics demonstration environment that allows the simulation of the lines of force produced by two charged particles.

StatiegeldCouponsApp - Android-based Statiegeld coupons keeper

StatiegeldCouponsAPI - Web API part for the StatiegeldCoupons project.

ScheduleBot - ITMO University schedule bot for Discord

Talks

Dedukti and Lambdapi

Radboud University: Proof Assistants course Jun 2025

Speakers: Mikhail Ushakov

Presentation about the Dedukti logical framework and the Lambdapi proof assistant, focusing on their role in solving the problem of interoperability of the proof systems. During the presentation, I discussed the theoretical and practical challenges in translating proofs across different logical foundations and demonstrated how Dedukti (Lambda-Pi calculus modulo theory) can serve as a unifying framework. This talk also included the practical demonstrations of translating Rocq proofs into the Dedukti and Lambdapi using the CoqInE tool.

MLTT: W-types

Radboud University: Type Theory and Coq course Nov 2024

Speakers: Mikhail Ushakov, Rutger Broekhof

Presentation on W-types in Per Martin-Löf Type Theory. Includes the explanation of their formation, elimination, and computation rules, reformulated using the Pure Type Systems notation. During the presentation, we demonstrated the correspondence between the formal rules and their Coq (Rocq) implementations, and illustrated the expressiveness of W-types through examples including finite sets, natural numbers, ordinal numbers, and binary trees. The talk emphasizes how the W-types can uniformly represent the inductive and recursive data structures within the framework of constructive type theory.