Description

I am a Computer Science M.Sc. student 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 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)
  • 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”

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.