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.
@InProceedings{GPCE26p60,
author = {Anna Herlihy and Amir Shaikhha and Anastasia Ailamaki and Martin Odersky},
title = {Modular Substructural Constraints for Embedded DSLs},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {60-71},
doi = {10.1145/3814885.3816411},
year = {2026},
}
Publisher's Version
Article: gpce26main-p5-p doi:10.1145/3814885.3816411
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.
@InProceedings{GPCE26p15,
author = {Julien Signoles and Khaoula Boukir and Amine Nasri},
title = {ATLAS: From Access conTrol Language to ACSL Specifications},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {15-26},
doi = {10.1145/3814885.3816415},
year = {2026},
}
Publisher's Version
Article: gpce26main-p19-p doi:10.1145/3814885.3816415
GPCE '26: "Executable Counterfactuals: ..."
Executable Counterfactuals: A Causal Calculus for Concurrent Systems (Keynote)
Georgiana Caltais
(University of Twente, Netherlands)
Modern software systems are increasingly concurrent, adaptive, and generative, yet our formal methods still focus primarily on describing what systems do rather than why particular behaviours arise. In this talk, I will present ongoing work on a causal calculus for concurrent systems that combines process algebra, modal logic, and intervention-based causality in the style of Halpern and Pearl.
The key idea is to treat causal interventions as executable transformations of process-algebraic specifications: changing a cause corresponds to syntactically redefining process variables and analysing the resulting counterfactual behaviours. This yields a multi-layered framework -the Causal Transition Calculus (CTC)- connecting process algebra, labelled transition systems, Hennessy-Milner logic, and actual causality.
The framework establishes a sound and complete correspondence between causal reasoning over process-algebraic models and their induced behavioural semantics. At the same time, it reveals an important limitation of standard behavioural equivalences: systems that are bisimilar may still differ under counterfactual analysis due to differences in their internal causal structure.
Beyond its foundational aspects, this work suggests new ways of viewing causality through the lens of operational semantics. In particular, counterfactual reasoning becomes executable: interventions correspond to syntactic transformations whose behavioural consequences can be formally analysed. This perspective raises broader questions about causal equivalence, explainability of concurrent behaviour, and how causal reasoning can be integrated into the specification of concurrent systems
@InProceedings{GPCE26p2,
author = {Georgiana Caltais},
title = {Executable Counterfactuals: A Causal Calculus for Concurrent Systems (Keynote)},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {2-2},
doi = {10.1145/3814885.3827600},
year = {2026},
}
Publisher's Version
Article: gpce26main-key2-p doi:10.1145/3814885.3827600
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.
@InProceedings{GPCE26p39,
author = {Jef Jacobs and Wolfgang De Meuter and Jens Nicolay},
title = {TurtleTalk: A DSL for Constraint-Based Turtle Graphics in Programmatic CAD},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {39-49},
doi = {10.1145/3814885.3816416},
year = {2026},
}
Publisher's Version
Article: gpce26main-p21-p doi:10.1145/3814885.3816416
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.
@InProceedings{GPCE26p3,
author = {Fabian Eger and Lukas Güthing and Kevin Feichtinger and Ina Schaefer},
title = {Comparing Solver Representations for Analyzing Cardinality-Based Feature Models},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {3-14},
doi = {10.1145/3814885.3816410},
year = {2026},
}
Publisher's Version
Article: gpce26main-p4-p doi:10.1145/3814885.3816410
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.
@InProceedings{GPCE26p3,
author = {Fabian Eger and Lukas Güthing and Kevin Feichtinger and Ina Schaefer},
title = {Comparing Solver Representations for Analyzing Cardinality-Based Feature Models},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {3-14},
doi = {10.1145/3814885.3816410},
year = {2026},
}
Publisher's Version
Article: gpce26main-p4-p doi:10.1145/3814885.3816410
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.
@InProceedings{GPCE26p3,
author = {Fabian Eger and Lukas Güthing and Kevin Feichtinger and Ina Schaefer},
title = {Comparing Solver Representations for Analyzing Cardinality-Based Feature Models},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {3-14},
doi = {10.1145/3814885.3816410},
year = {2026},
}
Publisher's Version
Article: gpce26main-p4-p doi:10.1145/3814885.3816410
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.
@InProceedings{GPCE26p94,
author = {Shadaj Laddad and Mingwei Samuel and Joseph M. Hellerstein},
title = {Stageleft: Multi-stage Programming in Standard Rust},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {94-106},
doi = {10.1145/3814885.3816414},
year = {2026},
}
Publisher's Version
Article: gpce26main-p18-p doi:10.1145/3814885.3816414
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.
@InProceedings{GPCE26p60,
author = {Anna Herlihy and Amir Shaikhha and Anastasia Ailamaki and Martin Odersky},
title = {Modular Substructural Constraints for Embedded DSLs},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {60-71},
doi = {10.1145/3814885.3816411},
year = {2026},
}
Publisher's Version
Article: gpce26main-p5-p doi:10.1145/3814885.3816411
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.
@InProceedings{GPCE26p39,
author = {Jef Jacobs and Wolfgang De Meuter and Jens Nicolay},
title = {TurtleTalk: A DSL for Constraint-Based Turtle Graphics in Programmatic CAD},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {39-49},
doi = {10.1145/3814885.3816416},
year = {2026},
}
Publisher's Version
Article: gpce26main-p21-p doi:10.1145/3814885.3816416
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.
@InProceedings{GPCE26p50,
author = {Arthur Jamet and Michael Vollmer},
title = {Programmable Record Types in Haskell},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {50-59},
doi = {10.1145/3814885.3816408},
year = {2026},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: gpce26main-p2-p doi:10.1145/3814885.3816408
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.
@InProceedings{GPCE26p72,
author = {Thomas Kottenhahn and Prashant Kumar},
title = {Metis: A Compositional DSL for Board Games and Game Tree Search},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {72-82},
doi = {10.1145/3814885.3816412},
year = {2026},
}
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: gpce26main-p7-p doi:10.1145/3814885.3816412
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.
@InProceedings{GPCE26p72,
author = {Thomas Kottenhahn and Prashant Kumar},
title = {Metis: A Compositional DSL for Board Games and Game Tree Search},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {72-82},
doi = {10.1145/3814885.3816412},
year = {2026},
}
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Article: gpce26main-p7-p doi:10.1145/3814885.3816412
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.
@InProceedings{GPCE26p94,
author = {Shadaj Laddad and Mingwei Samuel and Joseph M. Hellerstein},
title = {Stageleft: Multi-stage Programming in Standard Rust},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {94-106},
doi = {10.1145/3814885.3816414},
year = {2026},
}
Publisher's Version
Article: gpce26main-p18-p doi:10.1145/3814885.3816414
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.
@InProceedings{GPCE26p83,
author = {Junyu Lin and Akimasa Morihata},
title = {Synthesizing Recursive Functional Programs via Structure-Element Separation},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {83-93},
doi = {10.1145/3814885.3816413},
year = {2026},
}
Publisher's Version
Article: gpce26main-p13-p doi:10.1145/3814885.3816413
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.
@InProceedings{GPCE26p83,
author = {Junyu Lin and Akimasa Morihata},
title = {Synthesizing Recursive Functional Programs via Structure-Element Separation},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {83-93},
doi = {10.1145/3814885.3816413},
year = {2026},
}
Publisher's Version
Article: gpce26main-p13-p doi:10.1145/3814885.3816413
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.
@InProceedings{GPCE26p27,
author = {Krishna Narasimhan},
title = {Less Is More: Measuring How LLM Involvement Affects Chatbot Accuracy in Static Analysis},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {27-38},
doi = {10.1145/3814885.3816409},
year = {2026},
}
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Article: gpce26main-p3-p doi:10.1145/3814885.3816409
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.
@InProceedings{GPCE26p15,
author = {Julien Signoles and Khaoula Boukir and Amine Nasri},
title = {ATLAS: From Access conTrol Language to ACSL Specifications},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {15-26},
doi = {10.1145/3814885.3816415},
year = {2026},
}
Publisher's Version
Article: gpce26main-p19-p doi:10.1145/3814885.3816415
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.
@InProceedings{GPCE26p39,
author = {Jef Jacobs and Wolfgang De Meuter and Jens Nicolay},
title = {TurtleTalk: A DSL for Constraint-Based Turtle Graphics in Programmatic CAD},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {39-49},
doi = {10.1145/3814885.3816416},
year = {2026},
}
Publisher's Version
Article: gpce26main-p21-p doi:10.1145/3814885.3816416
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.
@InProceedings{GPCE26p60,
author = {Anna Herlihy and Amir Shaikhha and Anastasia Ailamaki and Martin Odersky},
title = {Modular Substructural Constraints for Embedded DSLs},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {60-71},
doi = {10.1145/3814885.3816411},
year = {2026},
}
Publisher's Version
Article: gpce26main-p5-p doi:10.1145/3814885.3816411
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.
@InProceedings{GPCE26p94,
author = {Shadaj Laddad and Mingwei Samuel and Joseph M. Hellerstein},
title = {Stageleft: Multi-stage Programming in Standard Rust},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {94-106},
doi = {10.1145/3814885.3816414},
year = {2026},
}
Publisher's Version
Article: gpce26main-p18-p doi:10.1145/3814885.3816414
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.
@InProceedings{GPCE26p3,
author = {Fabian Eger and Lukas Güthing and Kevin Feichtinger and Ina Schaefer},
title = {Comparing Solver Representations for Analyzing Cardinality-Based Feature Models},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {3-14},
doi = {10.1145/3814885.3816410},
year = {2026},
}
Publisher's Version
Article: gpce26main-p4-p doi:10.1145/3814885.3816410
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.
@InProceedings{GPCE26p60,
author = {Anna Herlihy and Amir Shaikhha and Anastasia Ailamaki and Martin Odersky},
title = {Modular Substructural Constraints for Embedded DSLs},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {60-71},
doi = {10.1145/3814885.3816411},
year = {2026},
}
Publisher's Version
Article: gpce26main-p5-p doi:10.1145/3814885.3816411
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.
@InProceedings{GPCE26p15,
author = {Julien Signoles and Khaoula Boukir and Amine Nasri},
title = {ATLAS: From Access conTrol Language to ACSL Specifications},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {15-26},
doi = {10.1145/3814885.3816415},
year = {2026},
}
Publisher's Version
Article: gpce26main-p19-p doi:10.1145/3814885.3816415
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.
@InProceedings{GPCE26p50,
author = {Arthur Jamet and Michael Vollmer},
title = {Programmable Record Types in Haskell},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {50-59},
doi = {10.1145/3814885.3816408},
year = {2026},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: gpce26main-p2-p doi:10.1145/3814885.3816408
GPCE '26: "Bringing Mixed-Stage Programming ..."
Bringing Mixed-Stage Programming to OCaml (Keynote)
Jeremy Yallop
(University of Cambridge, UK)
Over the last three decades, multi-stage programming has been used to write high-level, type-safe, optimising code generators for a wide variety of domains, from database queries and stream processing to geometry, parsing, and differentiable programming.
The Modular Macros project extends OCaml with new compile-time multi-stage programming features, enabling programmers to write code generators as functions that run during program compilation to produce efficient run-time code. These compile-time functions are deeply integrated into OCaml, with the same abstraction, safety, and modularity guarantees that shape the existing language design.
The central challenge lies in extending OCaml’s modules to support both run-time and compile-time components. This talk presents our higher-order mixed-stage module system as a solution to this challenge, and explores the insights for multi-stage language design and implementation that arise from taking modularity seriously.
@InProceedings{GPCE26p1,
author = {Jeremy Yallop},
title = {Bringing Mixed-Stage Programming to OCaml (Keynote)},
booktitle = {Proc.\ GPCE},
publisher = {ACM},
pages = {1-1},
doi = {10.1145/3814885.3827599},
year = {2026},
}
Publisher's Version
Article: gpce26main-key1-p doi:10.1145/3814885.3827599