@@ -24,20 +24,21 @@ My advisors are [Michael Kohlhase](https://kwarc.info/people/mkohlhase/) and [Fl
### Current Work
-**Master's Thesis:** 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 implementedoperators to systematically transform/translate/annotate diagrams of formalizations.
-**Master's Thesis:** 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: translation of sorted FOL-theories `T` to `Hom(T)` whose models are homomorphisms between `T`-models, i.e., 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))
- Translation of theories `T` to theories `Logrel(T)` that are "interface theories" 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)
-[*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)** (side project; 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/).
-**[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.
We formalize the latter in the MMT system and thus enable all the features that it already provides.
