university

Systematically deriving formalizations of extrinsic type theories from corresponding formalizations of the intrinsic variant

Reviewing the theory of logical relations formulated for logical frameworks by Rabe and Sojakova (2013) and presenting one possible instantiation in the MMT+Edinburgh LF system.

We can identify natural numbers with the multiset of their prime factors. The operations of GCD and LCM then correspond to multiset intersection and symmetric difference. We elaborate on this in great detail accessible to math & CS undergraduates.

Taking selected undergraduate material of math and CS that is classically taught with sets & functions and now presenting it with multisets & relations.

Research on concise specification and implementation of operators on diagrams of formalizations and their meta theory.

Project at KWARC connecting serious games and Mathematical Knowledge Management techniques.

Often meta-programming facilities that transform diagrams of formalizations adhere to a special form giving them nice meta propreties, e.g. preservation of includes (diagrammatic structure) and morphism composition.

I presented a talk at LFMTP on the utility of operators transforming diagrams of formalization in a meta-programming fashion. The talk corresponded to an extended abstract me and my advisor submitted.

Our paper on “detangling knowledge management from game design in serious games” was accepted.

Often meta-programming facilities that transform diagrams of formalizations adhere to a special form giving them nice meta propreties, e.g. preservation of includes (diagrammatic structure) and morphism composition.