Standard

Scopes as Types. / van Antwerpen, Hendrik; Bach Poulsen, Casper; Rouvoet, Arjen; Visser, Eelco.

In: Proceedings of the ACM on Programming Languages, Vol. 2, No. OOPSLA, 114, 2018, p. 1-30.

Research output: Contribution to journalArticleScientificpeer-review

Harvard

van Antwerpen, H, Bach Poulsen, C, Rouvoet, A & Visser, E 2018, 'Scopes as Types' Proceedings of the ACM on Programming Languages, vol. 2, no. OOPSLA, 114, pp. 1-30. https://doi.org/10.1145/3276484

APA

van Antwerpen, H., Bach Poulsen, C., Rouvoet, A., & Visser, E. (2018). Scopes as Types. Proceedings of the ACM on Programming Languages, 2(OOPSLA), 1-30. [114]. https://doi.org/10.1145/3276484

Vancouver

van Antwerpen H, Bach Poulsen C, Rouvoet A, Visser E. Scopes as Types. Proceedings of the ACM on Programming Languages. 2018;2(OOPSLA):1-30. 114. https://doi.org/10.1145/3276484

Author

van Antwerpen, Hendrik ; Bach Poulsen, Casper ; Rouvoet, Arjen ; Visser, Eelco. / Scopes as Types. In: Proceedings of the ACM on Programming Languages. 2018 ; Vol. 2, No. OOPSLA. pp. 1-30.

BibTeX

@article{9aad733b23d445d7b52f331b80c5d029,
title = "Scopes as Types",
abstract = "Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.",
author = "{van Antwerpen}, Hendrik and {Bach Poulsen}, Casper and Arjen Rouvoet and Eelco Visser",
year = "2018",
doi = "10.1145/3276484",
language = "English",
volume = "2",
pages = "1--30",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
number = "OOPSLA",

}

RIS

TY - JOUR

T1 - Scopes as Types

AU - van Antwerpen, Hendrik

AU - Bach Poulsen, Casper

AU - Rouvoet, Arjen

AU - Visser, Eelco

PY - 2018

Y1 - 2018

N2 - Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.

AB - Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.

U2 - 10.1145/3276484

DO - 10.1145/3276484

M3 - Article

VL - 2

SP - 1

EP - 30

JO - Proceedings of the ACM on Programming Languages

T2 - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - OOPSLA

M1 - 114

ER -

ID: 47192514