Newer
Older
---
layout: person
title: Navid Roux
fullname: B.Sc. Navid Roux
affiliation: Computer Science, FAU Erlangen-Nürnberg
github: ComFreek
orcid: 0000-0002-8348-2441
publink: auto
mathhub: NavidRoux
researchgate: Navid_Roux
website: https://navid-roux.netlify.app/
I am a Computer Science M.Sc. student ([they/he](http://pronoun.is/they?or=he)) with research interests in *knowledge representation and processing* of formal content
such as foundations, logics, type theories, and math.
My advisors are [Michael Kohlhase](https://kwarc.info/people/mkohlhase/) and [Florian Rabe](https://kwarc.info/people/frabe/)
- **Master's Thesis:** developing a framework of meta-programming operators on formalizations (in theory and [for the MMT system](https://kwarc.info/systems/mmt/)) that allows such operators to be easily specified, verified, and implemented. Operators translate specifications/theories/signatures over a logical framework to new ones.
- [*Systematic Translation of Formalizations of Type Theory
from Intrinsic to Extrinsic Style*](https://kwarc.info/people/frabe/Research/RR_softening_21.pdf) (joint work with Florian Rabe)
- Universal algebra: translating FOL-theories `T` to `Hom(T)` whose models are homomorphisms between `T`-models (=> automatic generation of, say, the theory of group homomorphisms from a specification `T = Group`); similarly translation of `T` to `Sub(T)`, `Cong(T)` whose models are substructures and congruences on `T`-models (see joint work with Florian Rabe: [*Structure-Preserving Diagram Operators*](https://kwarc.info/people/frabe/Research/RR_diagops_20.pdf))
- Translating specifications `T` of arbitrary formal systems in LF to `Logrel(T)` that is an "interface specification" for proofs by logical relations over `T`-syntax (e.g., `T` might formalize simply-typed lambda calculus and an implementation of `Logrel(T)` may be a proof of strong normalization)
- **Partial and higher-order logical relations for a logical framework** and representation therein (joint work with Florian Rabe): we used partial logical relations to translate Church-style formalizations of type theories to Curry-style ones, see ["Systematic Translation of Formalizations of Type Theory
from Intrinsic to Extrinsic Style"](https://kwarc.info/people/frabe/Research/RR_softening_21.pdf)
### Current Work on the side
- **[FrameIT](https://uframeit.org)** (see link for collaborators): developing a prototype of a serious educational game that exploits knowledge management and logic features of the [MMT system](https://kwarc.info/systems/mmt/).
That way, we separate developing the 3D game mechanics from encoding and management of the serious game contents.
We formalize the latter in the MMT system and thus enable all the features that it already provides.
Checking whether a player-entered solution is correct? Amounts to typechecking.
Composing multiple serious game contents? Amounts to combination of formalizations.
Translating serious game contents from one world to another? Amounts to a pushout in the formalization.
See our paper [*FrameIT: Detangling Knowledge Management from Game Design in Serious Games*](http://kwarc.info/kohlhase/submit/cicm20-frameit.pdf).
- **MMT ecosystem:** developing [tools](https://github.com/ComFreek/mmteditor) and [multiple syntax highlighters](https://github.com/ComFreek/mmtpygments) making one's life even more enjoyable with the MMT system.
- **Master's Seminar:** [*A Beginner's Guide to Logical Relations for a Logical Framework*](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/logrels/guide.pdf) ([slides](https://gl.kwarc.info/supervision/seminar/-/blob/master/WS2021/logrels/slides.pdf))
- **Master's Project:** [*Structure-Preserving Diagram Operators*](https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Roux_Navid.pdf)
- **Bachelor's Thesis:** [*Refactoring of Theory Graphs in Knowledge Representation Systems*](https://navid-roux.netlify.app/bsc-thesis/)
See [my personal website](https://navid-roux.netlify.app/) for Master's courses I have taken.