@@ -22,22 +22,22 @@ I am a Computer Science M.Sc. student with research interests in *knowledge repr
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/)
So far I have 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* formalization 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'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.
-**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 implementedoperators 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, …
Examples of operators:
-["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: translation of sorted FOL-theories `T` to `Hom(T)` whose models are homomorphisms between `T`-models, i.e., 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))
- Translation of theories `T` to theories `Logrel(T)` that are "interface theories" 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)** (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/).
-**[FrameIT](https://uframeit.org)** (side project; 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.
...
...
@@ -51,6 +51,7 @@ Besides my Master's studies, currently I am working…
### Previous Work
-**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))
