SPLASH 2020 (series) / SLE 2020 (series) / SLE (Software Language Engineering) 2020 /
Extrinsically Typed Operational Semantics for Functional Languages
Sun 15 Nov 2020 16:00 - 16:20 at SPLASH-III - Chair(s): Jonathan Aldrich
Mon 16 Nov 2020 04:00 - 04:20 at SPLASH-III - Chair(s): Erwan Bousse
Mon 16 Nov 2020 04:00 - 04:20 at SPLASH-III - Chair(s): Erwan Bousse
We present a type system over language definitions that classifies parts of the operational semantics of a language in input, and
models a common language design organization.
The resulting typing discipline guarantees that the language at hand is automatically type sound.
Thanks to the use of types to model language design,
our type checker has a high-level view on the language being
analyzed and can report messages using the same jargon of language designers.
We have implemented our type system in the $\textsc{lang-n-check}$ tool, and we have applied it to derive the type soundness of several functional languages, including those with recursive types, polymorphism, exceptions, lists, sums, and several common types and operators.
Sun 15 NovDisplayed time zone: Central Time (US & Canada) change
Sun 15 Nov
Displayed time zone: Central Time (US & Canada) change
Mon 16 NovDisplayed time zone: Central Time (US & Canada) change
Mon 16 Nov
Displayed time zone: Central Time (US & Canada) change