TY - GEN
T1 - Extrinsically typed operational semantics for functional languages
AU - Cimini, Matteo
AU - Miller, Dale
AU - Siek, Jeremy G.
N1 - Publisher Copyright:
© 2020 ACM.
PY - 2020/11/16
Y1 - 2020/11/16
N2 - 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 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.
AB - 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 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.
KW - Extrinsic type systems
KW - functional languages
KW - type soundness
U2 - 10.1145/3426425.3426936
DO - 10.1145/3426425.3426936
M3 - Conference contribution
AN - SCOPUS:85097710575
T3 - SLE 2020 - Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, Co-located with SPLASH 2020
SP - 108
EP - 125
BT - SLE 2020 - Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, Co-located with SPLASH 2020
A2 - Lammel, Ralf
A2 - Tratt, Laurence
A2 - de Lara, Juan
PB - Association for Computing Machinery, Inc
T2 - 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, co-located with SPLASH 2020
Y2 - 16 November 2020 through 17 November 2020
ER -