GPCE '26: "Modular Substructural Constraints ..."
Modular Substructural Constraints for Embedded DSLs
Anna Herlihy, Amir Shaikhha, Anastasia Ailamaki, and Martin Odersky
(EPFL, Switzerland; University of Edinburgh, UK)
Substructural type systems provide static guarantees about resource usage in programs. In most practical systems, however, the available usage constraints and their composition are predetermined by the language design, with only limited support for application programmers to customize them. We present a technique for expressing modular substructural constraints on function arrows in embedded domain-specific languages, enabling resource disciplines to be customized to the heterogeneous requirements of real-world domains. We formalize the design as an extension of the simply-typed lambda calculus and provide a Scala 3 implementation that uses type-level programming to enforce constraints at compile-time without host-compiler modifications. We illustrate the approach on a Linear Datalog case study, showing no performance overhead on practical programs.
Article Search
Article: gpce26main-p5-p
GPCE '26: "ATLAS: From Access conTrol ..."
ATLAS: From Access conTrol Language to ACSL Specifications
Julien Signoles, Khaoula Boukir, and Amine Nasri
(Université Paris-Saclay - CEA - List, France; Ibn Tofail University, Morocco)
Access control is a classical way to express which users are allowed to do which actions on which objects. Many formalisms study how to model access control policies. However, fewer works target formal verification of an actual implementation with respect to a given policy. This paper presents ATLAS, a new formal specification language for expressing access control policies. This language allows for modeling an access control policy, linking it to a source code, and generating automatically formal annotations in order to verify that a source code correctly implements the modeled policy. This workflow is implemented as a new Frama-C plugin that generates ACSL annotations, which can be proved by deductive verification or checked at runtime.
Article Search
Article: gpce26main-p19-p
GPCE '26: "TurtleTalk: A DSL for Constraint-Based ..."
TurtleTalk: A DSL for Constraint-Based Turtle Graphics in Programmatic CAD
Jef Jacobs, Wolfgang De Meuter, and Jens Nicolay
(Vrije Universiteit Brussel, Belgium)
In programmatic CAD (PCAD), 3D shapes are generally modelled either by position-based composition of simpler shapes, or by direct generation via path-based techniques (e.g., extrusions, sweeps, revolves). While state-of-the-art PCAD tools effectively support position-based modelling, they lack expressive mechanisms for path-based modelling. As a result, shapes that are naturally formed by sweeping a 2D path into a 3D shape are difficult to model and use in these tools. This paper introduces TurtleTalk, a PCAD language that offers rich support for constructing path-based shapes and the composition of path-based and primitive shapes. TurtleTalk is an extension of PrintTalk, a PCAD language featuring constraints for composing constituent shapes into complex 3D models. TurtleTalk takes inspiration from turtle graphics for constructing paths using imperative instructions and uniquely integrates constraints to enable the declarative expression of path properties. Our evaluation shows that combining imperative instructions and declarative constraints facilitates the design of path-based shapes by reducing the need for complex manual calculations, while also enhancing their composability and reusability.
Article Search
Article: gpce26main-p21-p
GPCE '26: "Comparing Solver Representations ..."
Comparing Solver Representations for Analyzing Cardinality-Based Feature Models
Fabian Eger, Lukas Güthing, Kevin Feichtinger, and Ina Schaefer
(KIT, Germany)
The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot be done with state-of-the-art, SAT-based tooling for analyzing Boolean Feature Models (FMs). Analyses on FMs include checking for satisfying configurations, dead features, false optional features, and whether specific configurations are valid according to the FM. In this work, we compare different solver encodings to enable analysis for CFMs. First, we generalize the analyses on Boolean FMs to the notion of cardinalities and the new anomalies that can occur. Second, we present three different mathematical encodings of CFMs for automated reasoning using solvers. Third, we implement the encoding for ILP, SMT, and CSP solvers. We evaluate the feasibility and performance of our encodings on current ILP, SMT, and CSP solvers. Our evaluation shows that our encoding for CSP solvers enables all common analyses with the best performance among the compared encodings and solvers.
Article Search
Article: gpce26main-p4-p
GPCE '26: "Comparing Solver Representations ..."
Comparing Solver Representations for Analyzing Cardinality-Based Feature Models
Fabian Eger, Lukas Güthing, Kevin Feichtinger, and Ina Schaefer
(KIT, Germany)
The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot be done with state-of-the-art, SAT-based tooling for analyzing Boolean Feature Models (FMs). Analyses on FMs include checking for satisfying configurations, dead features, false optional features, and whether specific configurations are valid according to the FM. In this work, we compare different solver encodings to enable analysis for CFMs. First, we generalize the analyses on Boolean FMs to the notion of cardinalities and the new anomalies that can occur. Second, we present three different mathematical encodings of CFMs for automated reasoning using solvers. Third, we implement the encoding for ILP, SMT, and CSP solvers. We evaluate the feasibility and performance of our encodings on current ILP, SMT, and CSP solvers. Our evaluation shows that our encoding for CSP solvers enables all common analyses with the best performance among the compared encodings and solvers.
Article Search
Article: gpce26main-p4-p
GPCE '26: "Comparing Solver Representations ..."
Comparing Solver Representations for Analyzing Cardinality-Based Feature Models
Fabian Eger, Lukas Güthing, Kevin Feichtinger, and Ina Schaefer
(KIT, Germany)
The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot be done with state-of-the-art, SAT-based tooling for analyzing Boolean Feature Models (FMs). Analyses on FMs include checking for satisfying configurations, dead features, false optional features, and whether specific configurations are valid according to the FM. In this work, we compare different solver encodings to enable analysis for CFMs. First, we generalize the analyses on Boolean FMs to the notion of cardinalities and the new anomalies that can occur. Second, we present three different mathematical encodings of CFMs for automated reasoning using solvers. Third, we implement the encoding for ILP, SMT, and CSP solvers. We evaluate the feasibility and performance of our encodings on current ILP, SMT, and CSP solvers. Our evaluation shows that our encoding for CSP solvers enables all common analyses with the best performance among the compared encodings and solvers.
Article Search
Article: gpce26main-p4-p
GPCE '26: "Stageleft: Multi-stage Programming ..."
Stageleft: Multi-stage Programming in Standard Rust
Shadaj Laddad, Mingwei Samuel, and Joseph M. Hellerstein
(Amazon Web Services, USA; University of California at Berkeley, USA)
Rust has emerged as a popular systems language with growing interest in metaprogramming, yet it lacks staging support—developers must write unsafe, untyped macros instead. We present Stageleft, a library that brings type-safe staged programming to standard Rust without compiler modifications. Stageleft ensures hygienic code generation through ahead-of-time AST analysis, and handles free variables via a trait system that respects Rust's ownership rules. Stageleft demonstrates that staging can be practical and safe in Rust, enabling domain-specific optimizations while maintaining familiar developer interfaces.
Article Search
Article: gpce26main-p18-p
GPCE '26: "Modular Substructural Constraints ..."
Modular Substructural Constraints for Embedded DSLs
Anna Herlihy, Amir Shaikhha, Anastasia Ailamaki, and Martin Odersky
(EPFL, Switzerland; University of Edinburgh, UK)
Substructural type systems provide static guarantees about resource usage in programs. In most practical systems, however, the available usage constraints and their composition are predetermined by the language design, with only limited support for application programmers to customize them. We present a technique for expressing modular substructural constraints on function arrows in embedded domain-specific languages, enabling resource disciplines to be customized to the heterogeneous requirements of real-world domains. We formalize the design as an extension of the simply-typed lambda calculus and provide a Scala 3 implementation that uses type-level programming to enforce constraints at compile-time without host-compiler modifications. We illustrate the approach on a Linear Datalog case study, showing no performance overhead on practical programs.
Article Search
Article: gpce26main-p5-p
GPCE '26: "TurtleTalk: A DSL for Constraint-Based ..."
TurtleTalk: A DSL for Constraint-Based Turtle Graphics in Programmatic CAD
Jef Jacobs, Wolfgang De Meuter, and Jens Nicolay
(Vrije Universiteit Brussel, Belgium)
In programmatic CAD (PCAD), 3D shapes are generally modelled either by position-based composition of simpler shapes, or by direct generation via path-based techniques (e.g., extrusions, sweeps, revolves). While state-of-the-art PCAD tools effectively support position-based modelling, they lack expressive mechanisms for path-based modelling. As a result, shapes that are naturally formed by sweeping a 2D path into a 3D shape are difficult to model and use in these tools. This paper introduces TurtleTalk, a PCAD language that offers rich support for constructing path-based shapes and the composition of path-based and primitive shapes. TurtleTalk is an extension of PrintTalk, a PCAD language featuring constraints for composing constituent shapes into complex 3D models. TurtleTalk takes inspiration from turtle graphics for constructing paths using imperative instructions and uniquely integrates constraints to enable the declarative expression of path properties. Our evaluation shows that combining imperative instructions and declarative constraints facilitates the design of path-based shapes by reducing the need for complex manual calculations, while also enhancing their composability and reusability.
Article Search
Article: gpce26main-p21-p
GPCE '26: "Programmable Record Types ..."
Programmable Record Types in Haskell
Arthur Jamet and Michael Vollmer
(University of Kent, UK)
In Haskell, accessing an object's fields requires deconstructing it. Thankfully, it is possible to name the fields of a data type using the record syntax, allowing programmers to access objects' fields using their name. This can help improve the readability of Haskell code. However, Haskell's support for record types is limited, as its type system is nominal, and the language does not allow composing record types.
Previous work tackled this issue using type-level computations at compile time and linked lists at runtime. Since these approaches do not use native record data types, operations on such records (e.g. traversals) are consequently slower than on native data types.
In this paper, we leverage meta-programming and code generation to enable easy record composition and simulate structural subtyping, using type-transforming functions and typeclasses generated at compile time. The resulting Haskell library, named type-machine, generates native record data types. Its API allows users to write their own functions to compose record types. Our approach does not require any compiler or runtime modifications.
Our benchmarks show that records generated by type-machine are at least 40% faster to traverse than records defined using state-of-the-art libraries. Additionally, simple programs that define data types using type-machine are at least 3x faster to compile than isomorphic programs that use these libraries.
We present use cases of the library along with examples of custom type transformers.
Article Search
Artifacts Available
Article: gpce26main-p2-p
GPCE '26: "Metis: A Compositional DSL ..."
Metis: A Compositional DSL for Board Games and Game Tree Search
Thomas Kottenhahn and Prashant Kumar
(University of Mainz, Germany)
We present Metis, a domain-specific language embedded in Haskell for two-player board games on rectangular boards that exploits their shared structure (setup, rules, win condition) through three composable mini-DSLs. Atomic operations for placing, moving, and capturing pieces combine with filters, union, and sequencing to form rulesets; win conditions and evaluation functions reuse the same compositional pattern. With just 13 rule expressions Metis can express 80% of games from a catalog of 168 abstract games. The structure also supports game-playing agents through composable search and evaluation components.
Article Search
Artifacts Available
Article: gpce26main-p7-p
GPCE '26: "Metis: A Compositional DSL ..."
Metis: A Compositional DSL for Board Games and Game Tree Search
Thomas Kottenhahn and Prashant Kumar
(University of Mainz, Germany)
We present Metis, a domain-specific language embedded in Haskell for two-player board games on rectangular boards that exploits their shared structure (setup, rules, win condition) through three composable mini-DSLs. Atomic operations for placing, moving, and capturing pieces combine with filters, union, and sequencing to form rulesets; win conditions and evaluation functions reuse the same compositional pattern. With just 13 rule expressions Metis can express 80% of games from a catalog of 168 abstract games. The structure also supports game-playing agents through composable search and evaluation components.
Article Search
Artifacts Available
Article: gpce26main-p7-p
GPCE '26: "Stageleft: Multi-stage Programming ..."
Stageleft: Multi-stage Programming in Standard Rust
Shadaj Laddad, Mingwei Samuel, and Joseph M. Hellerstein
(Amazon Web Services, USA; University of California at Berkeley, USA)
Rust has emerged as a popular systems language with growing interest in metaprogramming, yet it lacks staging support—developers must write unsafe, untyped macros instead. We present Stageleft, a library that brings type-safe staged programming to standard Rust without compiler modifications. Stageleft ensures hygienic code generation through ahead-of-time AST analysis, and handles free variables via a trait system that respects Rust's ownership rules. Stageleft demonstrates that staging can be practical and safe in Rust, enabling domain-specific optimizations while maintaining familiar developer interfaces.
Article Search
Article: gpce26main-p18-p
GPCE '26: "Synthesizing Recursive Functional ..."
Synthesizing Recursive Functional Programs via Structure-Element Separation
Junyu Lin and Akimasa Morihata
(University of Tokyo, Japan)
Synthesizing recursive functional programs over algebraic data types from input-output examples remains challenging, largely due to the explosion of structurally distinct candidates during search. We present a synthesis approach for structurally recursive list/tree transformations based on a structure-element separation viewpoint: a structure transformation that determines output shape, and element computations that determine the values placed into that shape. Our method first infers structural relationships from examples that describe per-step output-size evolution along recursive calls and uses them to prune partial programs during top-down enumeration. For candidates that are structurally feasible, we apply a diamond function that converts the remaining element-level holes into small local program-by-example subproblems, which are then solved using symbolic execution and output alignment, enabling early acceptance or rejection without expanding unrelated global constructs. We implement the approach in an OCaml prototype synthesizer and evaluate it on a suite of list and tree benchmarks drawn from prior work. The results show that our method substantially reduces expensive example checking and improves synthesis performance on recursive list/tree transformation programs.
Article Search
Article: gpce26main-p13-p
GPCE '26: "Synthesizing Recursive Functional ..."
Synthesizing Recursive Functional Programs via Structure-Element Separation
Junyu Lin and Akimasa Morihata
(University of Tokyo, Japan)
Synthesizing recursive functional programs over algebraic data types from input-output examples remains challenging, largely due to the explosion of structurally distinct candidates during search. We present a synthesis approach for structurally recursive list/tree transformations based on a structure-element separation viewpoint: a structure transformation that determines output shape, and element computations that determine the values placed into that shape. Our method first infers structural relationships from examples that describe per-step output-size evolution along recursive calls and uses them to prune partial programs during top-down enumeration. For candidates that are structurally feasible, we apply a diamond function that converts the remaining element-level holes into small local program-by-example subproblems, which are then solved using symbolic execution and output alignment, enabling early acceptance or rejection without expanding unrelated global constructs. We implement the approach in an OCaml prototype synthesizer and evaluate it on a suite of list and tree benchmarks drawn from prior work. The results show that our method substantially reduces expensive example checking and improves synthesis performance on recursive list/tree transformation programs.
Article Search
Article: gpce26main-p13-p
GPCE '26: "Less Is More: Measuring How ..."
Less Is More: Measuring How LLM Involvement Affects Chatbot Accuracy in Static Analysis
Krishna Narasimhan
(F1RE, Netherlands)
Large language models are increasingly used to make static analysis tools accessible through natural language, yet existing systems differ in how much they delegate to the LLM without treating the degree of delegation as an independent variable. We compare three architectures along a spectrum of LLM involvement for translating natural language to Joern’s Code Property Graph Query Language (): direct query generation (1), generation of a schema-constrained JSON intermediate representation (2), and tool-augmented agentic generation (3). These are evaluated on a benchmark of 20 code analysis tasks across three complexity tiers, using four open-weight models in a 2×2 design (two model families × two scales), each with three repetitions. The structured intermediate representation (2) achieves the highest result match rates across all four models, outperforming direct generation by 15–25 percentage points on large models. The agentic approach (3) ranks last on every model despite substantially higher token cost. The benefit of structured intermediates is most pronounced for large models; for small models, schema compliance becomes the bottleneck. These findings suggest that in formally structured domains, constraining the LLM’s output to a well-typed intermediate representation and delegating query construction to deterministic code yields better results than either unconstrained generation or iterative tool use.
Article Search
Article: gpce26main-p3-p
GPCE '26: "ATLAS: From Access conTrol ..."
ATLAS: From Access conTrol Language to ACSL Specifications
Julien Signoles, Khaoula Boukir, and Amine Nasri
(Université Paris-Saclay - CEA - List, France; Ibn Tofail University, Morocco)
Access control is a classical way to express which users are allowed to do which actions on which objects. Many formalisms study how to model access control policies. However, fewer works target formal verification of an actual implementation with respect to a given policy. This paper presents ATLAS, a new formal specification language for expressing access control policies. This language allows for modeling an access control policy, linking it to a source code, and generating automatically formal annotations in order to verify that a source code correctly implements the modeled policy. This workflow is implemented as a new Frama-C plugin that generates ACSL annotations, which can be proved by deductive verification or checked at runtime.
Article Search
Article: gpce26main-p19-p
GPCE '26: "TurtleTalk: A DSL for Constraint-Based ..."
TurtleTalk: A DSL for Constraint-Based Turtle Graphics in Programmatic CAD
Jef Jacobs, Wolfgang De Meuter, and Jens Nicolay
(Vrije Universiteit Brussel, Belgium)
In programmatic CAD (PCAD), 3D shapes are generally modelled either by position-based composition of simpler shapes, or by direct generation via path-based techniques (e.g., extrusions, sweeps, revolves). While state-of-the-art PCAD tools effectively support position-based modelling, they lack expressive mechanisms for path-based modelling. As a result, shapes that are naturally formed by sweeping a 2D path into a 3D shape are difficult to model and use in these tools. This paper introduces TurtleTalk, a PCAD language that offers rich support for constructing path-based shapes and the composition of path-based and primitive shapes. TurtleTalk is an extension of PrintTalk, a PCAD language featuring constraints for composing constituent shapes into complex 3D models. TurtleTalk takes inspiration from turtle graphics for constructing paths using imperative instructions and uniquely integrates constraints to enable the declarative expression of path properties. Our evaluation shows that combining imperative instructions and declarative constraints facilitates the design of path-based shapes by reducing the need for complex manual calculations, while also enhancing their composability and reusability.
Article Search
Article: gpce26main-p21-p
GPCE '26: "Modular Substructural Constraints ..."
Modular Substructural Constraints for Embedded DSLs
Anna Herlihy, Amir Shaikhha, Anastasia Ailamaki, and Martin Odersky
(EPFL, Switzerland; University of Edinburgh, UK)
Substructural type systems provide static guarantees about resource usage in programs. In most practical systems, however, the available usage constraints and their composition are predetermined by the language design, with only limited support for application programmers to customize them. We present a technique for expressing modular substructural constraints on function arrows in embedded domain-specific languages, enabling resource disciplines to be customized to the heterogeneous requirements of real-world domains. We formalize the design as an extension of the simply-typed lambda calculus and provide a Scala 3 implementation that uses type-level programming to enforce constraints at compile-time without host-compiler modifications. We illustrate the approach on a Linear Datalog case study, showing no performance overhead on practical programs.
Article Search
Article: gpce26main-p5-p
GPCE '26: "Stageleft: Multi-stage Programming ..."
Stageleft: Multi-stage Programming in Standard Rust
Shadaj Laddad, Mingwei Samuel, and Joseph M. Hellerstein
(Amazon Web Services, USA; University of California at Berkeley, USA)
Rust has emerged as a popular systems language with growing interest in metaprogramming, yet it lacks staging support—developers must write unsafe, untyped macros instead. We present Stageleft, a library that brings type-safe staged programming to standard Rust without compiler modifications. Stageleft ensures hygienic code generation through ahead-of-time AST analysis, and handles free variables via a trait system that respects Rust's ownership rules. Stageleft demonstrates that staging can be practical and safe in Rust, enabling domain-specific optimizations while maintaining familiar developer interfaces.
Article Search
Article: gpce26main-p18-p
GPCE '26: "Comparing Solver Representations ..."
Comparing Solver Representations for Analyzing Cardinality-Based Feature Models
Fabian Eger, Lukas Güthing, Kevin Feichtinger, and Ina Schaefer
(KIT, Germany)
The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot be done with state-of-the-art, SAT-based tooling for analyzing Boolean Feature Models (FMs). Analyses on FMs include checking for satisfying configurations, dead features, false optional features, and whether specific configurations are valid according to the FM. In this work, we compare different solver encodings to enable analysis for CFMs. First, we generalize the analyses on Boolean FMs to the notion of cardinalities and the new anomalies that can occur. Second, we present three different mathematical encodings of CFMs for automated reasoning using solvers. Third, we implement the encoding for ILP, SMT, and CSP solvers. We evaluate the feasibility and performance of our encodings on current ILP, SMT, and CSP solvers. Our evaluation shows that our encoding for CSP solvers enables all common analyses with the best performance among the compared encodings and solvers.
Article Search
Article: gpce26main-p4-p
GPCE '26: "Modular Substructural Constraints ..."
Modular Substructural Constraints for Embedded DSLs
Anna Herlihy, Amir Shaikhha, Anastasia Ailamaki, and Martin Odersky
(EPFL, Switzerland; University of Edinburgh, UK)
Substructural type systems provide static guarantees about resource usage in programs. In most practical systems, however, the available usage constraints and their composition are predetermined by the language design, with only limited support for application programmers to customize them. We present a technique for expressing modular substructural constraints on function arrows in embedded domain-specific languages, enabling resource disciplines to be customized to the heterogeneous requirements of real-world domains. We formalize the design as an extension of the simply-typed lambda calculus and provide a Scala 3 implementation that uses type-level programming to enforce constraints at compile-time without host-compiler modifications. We illustrate the approach on a Linear Datalog case study, showing no performance overhead on practical programs.
Article Search
Article: gpce26main-p5-p
GPCE '26: "ATLAS: From Access conTrol ..."
ATLAS: From Access conTrol Language to ACSL Specifications
Julien Signoles, Khaoula Boukir, and Amine Nasri
(Université Paris-Saclay - CEA - List, France; Ibn Tofail University, Morocco)
Access control is a classical way to express which users are allowed to do which actions on which objects. Many formalisms study how to model access control policies. However, fewer works target formal verification of an actual implementation with respect to a given policy. This paper presents ATLAS, a new formal specification language for expressing access control policies. This language allows for modeling an access control policy, linking it to a source code, and generating automatically formal annotations in order to verify that a source code correctly implements the modeled policy. This workflow is implemented as a new Frama-C plugin that generates ACSL annotations, which can be proved by deductive verification or checked at runtime.
Article Search
Article: gpce26main-p19-p
GPCE '26: "Programmable Record Types ..."
Programmable Record Types in Haskell
Arthur Jamet and Michael Vollmer
(University of Kent, UK)
In Haskell, accessing an object's fields requires deconstructing it. Thankfully, it is possible to name the fields of a data type using the record syntax, allowing programmers to access objects' fields using their name. This can help improve the readability of Haskell code. However, Haskell's support for record types is limited, as its type system is nominal, and the language does not allow composing record types.
Previous work tackled this issue using type-level computations at compile time and linked lists at runtime. Since these approaches do not use native record data types, operations on such records (e.g. traversals) are consequently slower than on native data types.
In this paper, we leverage meta-programming and code generation to enable easy record composition and simulate structural subtyping, using type-transforming functions and typeclasses generated at compile time. The resulting Haskell library, named type-machine, generates native record data types. Its API allows users to write their own functions to compose record types. Our approach does not require any compiler or runtime modifications.
Our benchmarks show that records generated by type-machine are at least 40% faster to traverse than records defined using state-of-the-art libraries. Additionally, simple programs that define data types using type-machine are at least 3x faster to compile than isomorphic programs that use these libraries.
We present use cases of the library along with examples of custom type transformers.
Article Search
Artifacts Available
Article: gpce26main-p2-p