diff --git a/people/nroux.md b/people/nroux.md index 619c212295413530d98126ab299d7180fa5a5aaa..6d9ccfdeec52515e005e919b359b9ee1d6db0cc4 100644 --- a/people/nroux.md +++ b/people/nroux.md @@ -18,17 +18,40 @@ website: https://navid-roux.netlify.app/ --- ### Description -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/) +- Master's Project: [*Structure-Preserving Diagram Operators*](https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Roux_Navid.pdf) -- …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. ### Contact