Formalizing the abstract definitions of semantics in MMT

Master / Vertiefung Wissensrepräsentation und -Verarbeitung
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Formalizing the abstract definitions of semantics in MMT
For fun I formalized the abstract definitions of deductive, computational, and concretized semantics in MMT.
You can find it here: https://gl.mathhub.info/MMT/LATIN2/-/tree/tetrapod/source/type_theory/tetrapod.

I also captured the interdefinabilities of the semantics as MMT views, see sample below.
It would be really cool to give actual proofs instead of the cheating [m]sketch “…”[/m] parts.