Description
I am a Computer Science M.Sc. student (they/he) with research interests in knowledge representation and processing of formal content such as foundations, logics, type theories, and math. My advisors are Michael Kohlhase and Florian Rabe
Current Work
-
Master’s Thesis: developing a framework of meta-programming operators on formalizations (in theory and for the MMT system) 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 (joint work with Florian Rabe)
- Universal algebra: translating FOL-theories
T
toHom(T)
whose models are homomorphisms betweenT
-models (=> automatic generation of, say, the theory of group homomorphisms from a specificationT = Group
); similarly translation ofT
toSub(T)
,Cong(T)
whose models are substructures and congruences onT
-models (see joint work with Florian Rabe: Structure-Preserving Diagram Operators) - Translating specifications
T
of arbitrary formal systems in LF toLogrel(T)
that is an “interface specification” for proofs by logical relations overT
-syntax (e.g.,T
might formalize simply-typed lambda calculus and an implementation ofLogrel(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”
Current Work on the side
-
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.
-
MMT ecosystem: developing tools and multiple syntax highlighters making one’s life even more enjoyable with the MMT system.
Previous Work
- 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
See my personal website for Master’s courses I have taken.
Contact
Feel free to contact me at firstname.lastname@fau.de
.