Recent & Upcoming Talks

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.

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.

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.

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.

Based on the foundation-independent module system MMT, I propose a general definition of behavior-preserving refactorings, and as the primary example give a method to generalize inversely along MMT morphisms (refinements).