Newer
Older
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 Navid ([they/he](http://pronoun.is/they?or=he)) and a research assistant at kwarc
currently funded on the [VollKI](https://kwarc.info/projects/voll-ki/) and [FrameIT project](https://kwarc.info/systems/frameit/).
My research interest is *knowledge representation and processing* of formal declarative languages including
foundations, logics, type and set theories, and math.
My work is heavily inspired and closely tied to the [MMT project](https://kwarc.info/systems/mmt/),
where I develop theory in the framework given by the [MMT language](https://uniformal.github.io/doc/language/)
and apply it in practice in the [MMT system](https://github.com/UniFormal/MMT) (a reference implementation and associated ecosystem of software).
I am advised by [Michael Kohlhase](https://kwarc.info/people/mkohlhase/) and [Florian Rabe](https://kwarc.info/people/frabe/).
- **[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).
- **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)
- **Publications (selection):** click on the bibliography icon on the right.
- [*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)
- [*FrameIT: Detangling Knowledge Management from Game Design in Serious Games*](https://kwarc.info/kohlhase/papers/cicm20-frameit.pdf) (joint work with Michael Kohlhase and many more authors, see link)
- **Master's Thesis:** [A Framework for Defining Structure-Preserving Diagram Operators](https://gl.kwarc.info/supervision/MSc-archive/-/blob/master/2022/RouxNavid.pdf) (todo: links to corrupted pdf) ([slides](https://gl.kwarc.info/NavidRoux/seminar/-/blob/c73c6362a195a5e8d57c2723e179df04f3d5960b/SS2022/diagops/slides.pdf))
- **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/e1b1ea2fd5eb8d4d864140cddf20a9ca28397583/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/) ([slides](https://gl.kwarc.info/NavidRoux/seminar/-/blob/26d392e0eabff2e3c27de12fddd40dbe3823808c/SS2019/refactoring-theory-graphs/slides.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.
See [my personal website](https://navid-roux.netlify.app/) for Master's courses I have taken.