Description

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.

Current Work

• 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”

Previous Work

• Publications (selection): click on the bibliography icon on the right.
  • Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style (joint work with Florian Rabe)
  • FrameIT: Detangling Knowledge Management from Game Design in Serious Games (joint work with Michael Kohlhase and many more authors, see link)
• Master’s Thesis: A Framework for Defining Structure-Preserving Diagram Operators (todo: links to corrupted pdf) (slides)
• Master’s Seminar: A Beginner’s Guide to Logical Relations for a Logical Framework (slides)
• Master’s Project: Structure-Preserving Diagram Operators
• Bachelor’s Thesis: Refactoring of Theory Graphs in Knowledge Representation Systems (slides)
• MMT ecosystem: developing tools and multiple syntax highlighters making one’s life even more enjoyable with the MMT system.

See my personal website for Master’s courses I have taken.

Contact

Feel free to contact me at firstname.lastname@fau.de.