From 2741676e3b38b275f9399a900c46d476c8ddc9df Mon Sep 17 00:00:00 2001 From: Navid Roux <navid.roux@fau.de> Date: Thu, 19 Jan 2023 19:58:07 +0000 Subject: [PATCH] Update nroux.md --- people/nroux.md | 34 ++++++++++++++++------------------ 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/people/nroux.md b/people/nroux.md index 9995b8c..0ca659b 100644 --- a/people/nroux.md +++ b/people/nroux.md @@ -18,26 +18,17 @@ website: https://navid-roux.netlify.app/ --- ### Description -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)) - **Master's Project:** [*Structure-Preserving Diagram Operators*](https://gl.kwarc.info/supervision/projectarchive/-/blob/master/2020/Roux_Navid.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. -- GitLab