I am a Master student at [FAU Erlangen-Nürnberg](https://www.fau.eu/), where I previously completed my B.Sc. degree with a thesis on [*Refactoring of Theory Graphs in Knowledge Representation Systems*](https://navid-roux.netlify.app/post/bsc-thesis/).
My primary interests lie in the field of *Mathematical Knowledge Management* (MKM), where I like to apply and extend existing formal methods, such as [KWARC's MMT system](https://kwarc.info/systems/mmt/), to facilitate formalization and reuse of knowledge. Moreover, I find parallels to software engineering fascinating: correctness, refactoring, and prototyping all have a very pragmatic side from a programmer's perspective as well as a formal side within the realm of MKM and theorem provers. Last but not least, both fields require good UX for programmers/formalizers, which led me to learning and caring about non-text-based programming languages by means of [projectional editing](https://martinfowler.com/bliki/ProjectionalEditing.html).
I am a Computer Science M.Sc. student with research interests in *knowledge representation and processing* of logics, type theories, and math.
I completed my Bachelor's thesis on [*Refactoring of Theory Graphs in Knowledge Representation Systems*](https://navid-roux.netlify.app/post/bsc-thesis/),
my Master's project on [*Structure-Preserving Diagram Operators*](https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Roux_Navid.pdf), and am currently working on extending the latter for my Master's thesis.
Common to all three works is the idea to first identify annoyances when trying to represent a very concrete thing
(e.g. getting a *concise* formalziation of algebra)
and to then develop scalable solutions that are as general as possible in the setting of the .
The latter mostly happens in the [MMT system](https://kwarc.info/systems/mmt/) paired with the [Edinburgh Logical Framework](https://en.wikipedia.org/wiki/Logical_framework#LF).
### Current Work
Besides my Master studies, currently I am working…
Besides my Master's studies, currently I am working…
- Master's Thesis: developing a framework of diagram operators, both in theory and in the [MMT system](https://kwarc.info/systems/mmt/), that allows operators to systematically transform/translate/annotate diagrams of formalizations.
With such a framework, we can concisely specify operators that translate formalizations of extensional type theory to formalizations of intensional type theories, or formalizations of FOL to sorted FOL, …
-[FrameIT](https://uframeit.org)(side project joined at kwarc): 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 and syntax highlighters making one's life even more enjoyable with the MMT system.
### Previous Work
- …on extending previous work on [diagram operators](https://kwarc.info/people/frabe/Research/RS_diagops_19.pdf), which allow taking a pre-existing formalization (as a diagram) and transforming it in useful ways to another diagram, e.g. to consistently *Abelianize* a formalization of general, non-Abelian universal algebra.
- Bachelor's Thesis: [*Refactoring of Theory Graphs in Knowledge Representation Systems*](https://navid-roux.netlify.app/post/bsc-thesis/)
- …with other KWARCies in the [FrameIT project](https://UFrameIT.github.io/) on exploiting MKM techniques for serious educational games. See our latest paper submission [*FrameIT: Detangling Knowledge Management from Game Design in Serious Games*](http://kwarc.info/kohlhase/submit/cicm20-frameit.pdf).
See [my personal website](https://navid-roux.netlify.app/) for Master's courses I have taken.
