formal-systems

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.

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.

Hobby exploration of the language workbench JetBrains MPS that allows to quickly create DSLs with a “projectional editing”-first idiom.

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.

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 on a yet unsubmitted paper from me and my advisor for which our extended abstract was accepted.

Informal talk highlighting some problems of naive composition of programming languages (e.g. SQL, HTML, and regex injections) and then introducing JetBrains MPS – a language workbench tool allowing to compose languages very easily.