I am Navid (they/he) and a research assistant at kwarc currently funded on the VollKI and FrameIT project. 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, where I develop theory in the framework given by the MMT language and apply it in practice in the MMT system (a reference implementation and associated ecosystem of software). I am advised by Michael Kohlhase and Florian Rabe.
FrameIT (see link for collaborators): developing a prototype of a serious educational game that exploits knowledge management and logic features of the MMT system.
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.
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”
See my personal website for Master’s courses I have taken.
Feel free to contact me at