-
Defining Name Accessibility using Scope Graphs (Extended Edition)
Authors:
Aron Zwaan,
Casper Bach Poulsen
Abstract:
Many programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private to indicate where it can be accessed. Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings, few existing type systems provide a formal account of name accessibility.
We present…
▽ More
Many programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private to indicate where it can be accessed. Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings, few existing type systems provide a formal account of name accessibility.
We present a declarative, executable, and language-parametric model for name accessibility, which provides a formal specification of name accessibility in Java, C#, C++, Rust, and Eiffel. We achieve this by defining name accessibility as a predicate on resolution paths through scope graphs. Since scope graphs are a language-independent model of name resolution, our model provides a uniform approach to defining different accessibility policies for different languages.
Our model is implemented in Statix, a logic language for executable type system specification using scope graphs. We evaluate its correctness on a test suite that compares it with the C#, Java, and Rust compilers, and show we can synthesize access modifiers in programs with holes accurately.
△ Less
Submitted 12 July, 2024;
originally announced July 2024.
-
Types and Semantics for Extensible Data Types (Extended Version)
Authors:
Cas van der Rest,
Casper Bach Poulsen
Abstract:
Developing and maintaining software commonly requires (1) adding new data type constructors to existing applications, but also (2) adding new functions that work on existing data. Most programming languages have native support for defining data types and functions in a way that supports either (1) or (2), but not both. This lack of native support makes it difficult to use and extend libraries. A t…
▽ More
Developing and maintaining software commonly requires (1) adding new data type constructors to existing applications, but also (2) adding new functions that work on existing data. Most programming languages have native support for defining data types and functions in a way that supports either (1) or (2), but not both. This lack of native support makes it difficult to use and extend libraries. A theoretically well-studied solution is to define data types and functions using initial algebra semantics. While it is possible to encode this solution in existing programming languages, such encodings add syntactic and interpretive overhead, and commonly fail to take advantage of the map and fold fusion laws of initial algebras which compilers could exploit to generate more efficient code. A solution to these is to provide native support for initial algebra semantics. In this paper, we develop such a solution and present a type discipline and core calculus for a language with native support for initial algebra semantics.
△ Less
Submitted 26 September, 2023;
originally announced September 2023.
-
Handling Higher-Order Effects
Authors:
Cas van der Rest,
Jaro Reinders,
Casper Bach Poulsen
Abstract:
Algebraic effect handlers is a programming paradigm where programmers can declare their own syntactic operations, and modularly define the semantics of these using effect handlers.
However, we cannot directly define algebraic effect handlers for many higher-order operations (or higher-order effects) -- i.e., operations that have computations as parameters.
Examples of such higher-order effects…
▽ More
Algebraic effect handlers is a programming paradigm where programmers can declare their own syntactic operations, and modularly define the semantics of these using effect handlers.
However, we cannot directly define algebraic effect handlers for many higher-order operations (or higher-order effects) -- i.e., operations that have computations as parameters.
Examples of such higher-order effects include common programming features, such as try-catch exception handlers, function abstraction, and more.
In this paper we present a new kind of effect handler that addresses this shortcoming.
Our effect handler approach is closely related to previous work on scoped effect handlers, which also supports higher-order effects.
A key difference is that our effect handlers make it easy to understand separate (higher-order) effects as separate concerns, since effects do not interact.
In contrast, effect interaction is the default with scoped effect handlers.
While separate concerns is the default with our handlers, it is also possible to define handlers where effects interact.
△ Less
Submitted 7 March, 2022;
originally announced March 2022.
-
SciNote: Collaborative Problem Solving and Argumentation Tool
Authors:
Janet Rafner,
Arthur Hjorth,
Carrie Weidner,
Shaeema Zaman Ahmed,
Christian Poulsen,
Clemens Klokmose,
Jacob Sherson
Abstract:
As educators push for students to learn science by doing science, there is a need for computational scaffolding to assist students' evaluation of scientific evidence and argument building. In this paper, we present a pilot study of SciNote, a CSCL tool allowing educators to integrate third-party software into a flexible and collaborative workspace. We explore how SciNote enables teams to build dat…
▽ More
As educators push for students to learn science by doing science, there is a need for computational scaffolding to assist students' evaluation of scientific evidence and argument building. In this paper, we present a pilot study of SciNote, a CSCL tool allowing educators to integrate third-party software into a flexible and collaborative workspace. We explore how SciNote enables teams to build data-driven arguments during inquiry-based learning activities.
△ Less
Submitted 7 April, 2021;
originally announced May 2021.
-
Scaling of transmission capacities in coarse-grained renewable electricity networks
Authors:
Mirko Schäfer,
Simon Bugge Siggaard,
Kun Zhu,
Chris Risager Poulsen,
Martin Greiner
Abstract:
Network models of large-scale electricity systems feature only a limited spatial resolution, either due to lack of data or in order to reduce the complexity of the problem with respect to numerical calculations. In such cases, both the network topology, the load and the generation patterns below a given spatial scale are aggregated into representative nodes. This coarse-graining affects power flow…
▽ More
Network models of large-scale electricity systems feature only a limited spatial resolution, either due to lack of data or in order to reduce the complexity of the problem with respect to numerical calculations. In such cases, both the network topology, the load and the generation patterns below a given spatial scale are aggregated into representative nodes. This coarse-graining affects power flows and thus the resulting transmission needs of the system. We derive analytical scaling laws for measures of network transmission capacity and cost in coarse-grained renewable electricity networks. For the cost measure only a very weak scaling with the spatial resolution of the system is found. The analytical results are shown to describe the scaling of the transmission infrastructure measures for a simplified, but data-driven and spatially detailed model of the European electricity system with a high share of fluctuating renewable generation.
△ Less
Submitted 21 September, 2017;
originally announced September 2017.
-
Flag-Based Big-Step Semantics
Authors:
Casper Bach Poulsen,
Peter D. Mosses
Abstract:
Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules a…
▽ More
Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature.
△ Less
Submitted 10 May, 2016;
originally announced May 2016.
