I ([they/he](http://pronoun.is/they?or=he)) am a research assistant at kwarc after having previously obtained my M.Sc. degree at FAU. My primary research interest is *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/)
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/).
### Current Work
-**Master's Thesis:** (todo: long submitted, need to update this website) 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.
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: 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.
...
...
@@ -48,13 +39,20 @@ from Intrinsic to Extrinsic Style"](https://kwarc.info/people/frabe/Research/RR_
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.
-**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)
### Previous Work
-**Publications:** 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)
-**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)
-**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))
-**Bachelor's Thesis:**[*Refactoring of Theory Graphs in Knowledge Representation Systems*](https://navid-roux.netlify.app/bsc-thesis/)
-**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.
