Programming Journal, Volume 11, Issue 3 – Author Index |
Contents -
Abstracts -
Authors
|
| Alsubhi, Arwa Hameed |
Arwa Hameed Alsubhi, Friederike Bruns, Ornela Dardha, and Simon J. Gay (University of Glasgow, UK; University of Oldenburg, Germany) Ensuring embedded systems satisfy both behavioural protocols and timing requirements on deployed hardware is challenging, particularly when such properties are analysed separately. This often leads developers to rely on late-stage profiling and testing, where timing violations may be discovered late in development or after deployment. We present TimedCoconut, a GCC-based verification toolchain that extends C++ behavioural protocols, i.e. typestates, with transition-level timing constraints. TimedCoconut enables programmers to specify both permitted sequences of operations and their temporal bounds directly at the type level. Verification proceeds in two compile-time phases. First, TimedCoconut checks operation ordering and potential logical timing problems against the declared timed typestate, independently of the target hardware. Second, it invokes the Bound-T WCET analysis tool to validate that the compiled program satisfies the declared timing bounds on the selected target platform. We evaluate TimedCoconut on five time-critical embedded applications running on two target platforms, ARM and AVR. The results show that measured execution times remain within the predicted WCET bounds, demonstrating that TimedCoconut provides safe over-approximations of execution time while enforcing both behavioural and timing constraints. This shifts timing validation from late-stage hardware testing to compile-time checking of timed typestate protocols against target-specific execution bounds. |
|
| Böhme, Lukas |
Toni Mattis, Benjamin Frost, Lukas Böhme, and Robert Hirschfeld (Hasso Plattner Institute, Germany; University of Potsdam, Germany) Programming often benefits from dynamic information that complements source code. In particular, program comprehension can take advantage of concrete run-time data whose structure and changes give meaning to abstract identifiers and computational steps. Obtaining up-to-date run-time information from a part of a system poses a number of challenges: First, a suitable entry point from which to run the code in question is needed. Second, such an entry point might require an explicit setup and expect specific input to reveal the behavior of interest. Third, execution should be repeatable to react immediately to code or input changes. In example-based live programming (ELP), programmers can attach concrete examples to parts of a program to receive continuous, up-to-date feedback as their program unfolds. To reduce the manual effort involved in example construction, recent approaches either reuse run-time data mined from previous executions or construct synthetic inputs. Reusing observed examples lacks control over their content, whereas synthetic input does not yet scale to larger domain models. Our approach extends ELP with user-configurable, generated examples that scale to complex object graphs. In contrast to previous generation strategies using large language models (LLMs) with static context, we let an LLM guide the exploration of a code base to construct the required context and validate and refine proposed examples using execution feedback. We evaluated our example-generation agent on a synthetic dataset of 12 programs with varying complexity, and validated it on 4 real-world projects, demonstrating that the vast majority of functions and branches can be reached through a generated example. We found that execution feedback enabled smaller, locally hosted models to reach the performance of frontier models, while numeric and formal reasoning remained a consistent weakness across LLMs. We further developed a prototype that integrates our example-generation agent into an ELP system in Visual Studio Code. Our exploratory intra-subject study (n = 8) using program comprehension tasks, comparing our prototype to GitHub Copilot as the baseline, revealed that participants trusted their acquired knowledge more when ad-hoc examples were available and used the tool like a lightweight debugger, while Copilot was perceived as providing more accessible, but less reliable predictions rather than execution-grounded observations. However, we found no effect on the correctness of answers to program comprehension questions. In connection with existing ELP systems and AI assistants, automating example generation can achieve ubiquitous run-time feedback available to both programmers and AI. |
|
| Bruns, Friederike |
Arwa Hameed Alsubhi, Friederike Bruns, Ornela Dardha, and Simon J. Gay (University of Glasgow, UK; University of Oldenburg, Germany) Ensuring embedded systems satisfy both behavioural protocols and timing requirements on deployed hardware is challenging, particularly when such properties are analysed separately. This often leads developers to rely on late-stage profiling and testing, where timing violations may be discovered late in development or after deployment. We present TimedCoconut, a GCC-based verification toolchain that extends C++ behavioural protocols, i.e. typestates, with transition-level timing constraints. TimedCoconut enables programmers to specify both permitted sequences of operations and their temporal bounds directly at the type level. Verification proceeds in two compile-time phases. First, TimedCoconut checks operation ordering and potential logical timing problems against the declared timed typestate, independently of the target hardware. Second, it invokes the Bound-T WCET analysis tool to validate that the compiled program satisfies the declared timing bounds on the selected target platform. We evaluate TimedCoconut on five time-critical embedded applications running on two target platforms, ARM and AVR. The results show that measured execution times remain within the predicted WCET bounds, demonstrating that TimedCoconut provides safe over-approximations of execution time while enforcing both behavioural and timing constraints. This shifts timing validation from late-stage hardware testing to compile-time checking of timed typestate protocols against target-specific execution bounds. |
|
| Dardha, Ornela |
Arwa Hameed Alsubhi, Friederike Bruns, Ornela Dardha, and Simon J. Gay (University of Glasgow, UK; University of Oldenburg, Germany) Ensuring embedded systems satisfy both behavioural protocols and timing requirements on deployed hardware is challenging, particularly when such properties are analysed separately. This often leads developers to rely on late-stage profiling and testing, where timing violations may be discovered late in development or after deployment. We present TimedCoconut, a GCC-based verification toolchain that extends C++ behavioural protocols, i.e. typestates, with transition-level timing constraints. TimedCoconut enables programmers to specify both permitted sequences of operations and their temporal bounds directly at the type level. Verification proceeds in two compile-time phases. First, TimedCoconut checks operation ordering and potential logical timing problems against the declared timed typestate, independently of the target hardware. Second, it invokes the Bound-T WCET analysis tool to validate that the compiled program satisfies the declared timing bounds on the selected target platform. We evaluate TimedCoconut on five time-critical embedded applications running on two target platforms, ARM and AVR. The results show that measured execution times remain within the predicted WCET bounds, demonstrating that TimedCoconut provides safe over-approximations of execution time while enforcing both behavioural and timing constraints. This shifts timing validation from late-stage hardware testing to compile-time checking of timed typestate protocols against target-specific execution bounds. |
|
| Flatt, Matthew |
Shriram Krishnamurthi and Matthew Flatt (Brown University, USA; University of Utah, USA) Context For decades, programming language implementors have designed error messages with one consumer in mind: the human programmer. Human-factors research has consistently found that programmers engage with error messages poorly—they skim, miss key information, and are easily overwhelmed. A practical consequence has been a strong design pressure toward brevity so that programmers will actually read them. Inquiry AI coding agents are now a second consumer of error messages. Unlike humans, agents will read large quantities of prose; the only practical limit on message size is the context window, and modern context windows are large. This raises a question the programming-language community has not previously had reason to ask: should error-message detail be calibrated differently for AI agents than for humans? Approach We investigate this question through a controlled experiment using Shplait, an ML-style statically typed language. We construct a suite of programs containing a single deliberate type error each, and measure how often an AI agent repairs them under ablation: a detailed error context; a proximate error location; a minimal type error; and a dynamic (test suite) error only. An automated oracle uses a combination of a type checker and a test suite to classify each modified program as having a type error, being type-correct but semantically incorrect, or being semantically correct. Knowledge We find concrete evidence that more detailed error messages generally improve an agent’s ability to fix type errors. We also see evidence that agents are able to fix programs whose names have all been obfuscated. Grounding Our primary experiment comprises 2,400 trials across ten complete runs, using both qwen2.5-coder:14b (a quality open-weight model) and claude-haiku-4.5 (a quality commercial model) via ollama and aider on dedicated GPU hardware. The experimental platform—correct programs, their erroneous counterparts, error modes, and oracle—is described in full. Importance If more detailed error messages genuinely help AI agents, then languages designed with only human readers in mind may be providing a suboptimal experience for AI coding. Our results suggest that it is worth considering offering two reporting modes: a terse human mode and a detailed AI mode. More broadly, we believe that language-model-targeted error-message design is an open and important design problem. |
|
| Fowler, Simon |
Olivia Weston and Simon Fowler (University of Glasgow, UK) Context Behavioural type systems such as session types, typestate, and mailbox types allow a developer to specify and check behavioural properties within their application code, giving programs that are correct-by-construction. Session types in particular allow a developer that communication in their code follows pre-defined protocols. Inquiry Implementing session types in functional languages requires some form of resource control, most commonly achieved through the use of linear typing. However, linear type systems as specified declaratively cannot be implemented algorithmically. Even when using techniques such as leftover typing, implementing other substructural modes (e.g., affine and relevant) requires ad-hoc changes to typing rules. Approach We investigate co-contextual type systems as a general framework for implementing substructural type systems. Whereas standard type systems require a type environment as an input to a typechecking algorithm, co-contextual type systems—a class of type system originally introduced for efficient incremental typechecking—produce a type environment as an output of the typechecking judgement. Knowledge We show how to generalise co-contextual type systems to support algorithmic implementations of substructural typing: simple changes to typechecker parameters allow us to instantiate our typechecker to check unrestricted, linear, affine, and relevant λ-calculi. Building on this approach, we present a second language with an extended constraint system that can support mixed-linearity typing, and we use this to implement an algorithmic type system for the GV session-typed functional language. Grounding We prove four instantiations of our algorithm sound and complete with respect to declarative unrestricted, linear, affine, and relevant λ-calculi. We prove our our co-contextual session typing algorithm sound and complete with respect to a declarative presentation of GV. Finally, we implement our typechecking algorithm in OCaml and demonstrate it on a series of case study applications. Importance This work shows the versatility of co-contextual typing as a framework for supporting algorithmic implementations of substructural type systems, in addition to its originally-presented benefits (e.g., support for incremental and parallel typechecking). Our work further lays the groundwork for implementing programming languages with more sophisticated type combination operations that are out-of-reach of current approaches. |
|
| Frost, Benjamin |
Toni Mattis, Benjamin Frost, Lukas Böhme, and Robert Hirschfeld (Hasso Plattner Institute, Germany; University of Potsdam, Germany) Programming often benefits from dynamic information that complements source code. In particular, program comprehension can take advantage of concrete run-time data whose structure and changes give meaning to abstract identifiers and computational steps. Obtaining up-to-date run-time information from a part of a system poses a number of challenges: First, a suitable entry point from which to run the code in question is needed. Second, such an entry point might require an explicit setup and expect specific input to reveal the behavior of interest. Third, execution should be repeatable to react immediately to code or input changes. In example-based live programming (ELP), programmers can attach concrete examples to parts of a program to receive continuous, up-to-date feedback as their program unfolds. To reduce the manual effort involved in example construction, recent approaches either reuse run-time data mined from previous executions or construct synthetic inputs. Reusing observed examples lacks control over their content, whereas synthetic input does not yet scale to larger domain models. Our approach extends ELP with user-configurable, generated examples that scale to complex object graphs. In contrast to previous generation strategies using large language models (LLMs) with static context, we let an LLM guide the exploration of a code base to construct the required context and validate and refine proposed examples using execution feedback. We evaluated our example-generation agent on a synthetic dataset of 12 programs with varying complexity, and validated it on 4 real-world projects, demonstrating that the vast majority of functions and branches can be reached through a generated example. We found that execution feedback enabled smaller, locally hosted models to reach the performance of frontier models, while numeric and formal reasoning remained a consistent weakness across LLMs. We further developed a prototype that integrates our example-generation agent into an ELP system in Visual Studio Code. Our exploratory intra-subject study (n = 8) using program comprehension tasks, comparing our prototype to GitHub Copilot as the baseline, revealed that participants trusted their acquired knowledge more when ad-hoc examples were available and used the tool like a lightweight debugger, while Copilot was perceived as providing more accessible, but less reliable predictions rather than execution-grounded observations. However, we found no effect on the correctness of answers to program comprehension questions. In connection with existing ELP systems and AI assistants, automating example generation can achieve ubiquitous run-time feedback available to both programmers and AI. |
|
| Gay, Simon J. |
Arwa Hameed Alsubhi, Friederike Bruns, Ornela Dardha, and Simon J. Gay (University of Glasgow, UK; University of Oldenburg, Germany) Ensuring embedded systems satisfy both behavioural protocols and timing requirements on deployed hardware is challenging, particularly when such properties are analysed separately. This often leads developers to rely on late-stage profiling and testing, where timing violations may be discovered late in development or after deployment. We present TimedCoconut, a GCC-based verification toolchain that extends C++ behavioural protocols, i.e. typestates, with transition-level timing constraints. TimedCoconut enables programmers to specify both permitted sequences of operations and their temporal bounds directly at the type level. Verification proceeds in two compile-time phases. First, TimedCoconut checks operation ordering and potential logical timing problems against the declared timed typestate, independently of the target hardware. Second, it invokes the Bound-T WCET analysis tool to validate that the compiled program satisfies the declared timing bounds on the selected target platform. We evaluate TimedCoconut on five time-critical embedded applications running on two target platforms, ARM and AVR. The results show that measured execution times remain within the predicted WCET bounds, demonstrating that TimedCoconut provides safe over-approximations of execution time while enforcing both behavioural and timing constraints. This shifts timing validation from late-stage hardware testing to compile-time checking of timed typestate protocols against target-specific execution bounds. |
|
| Hirschfeld, Robert |
Toni Mattis, Benjamin Frost, Lukas Böhme, and Robert Hirschfeld (Hasso Plattner Institute, Germany; University of Potsdam, Germany) Programming often benefits from dynamic information that complements source code. In particular, program comprehension can take advantage of concrete run-time data whose structure and changes give meaning to abstract identifiers and computational steps. Obtaining up-to-date run-time information from a part of a system poses a number of challenges: First, a suitable entry point from which to run the code in question is needed. Second, such an entry point might require an explicit setup and expect specific input to reveal the behavior of interest. Third, execution should be repeatable to react immediately to code or input changes. In example-based live programming (ELP), programmers can attach concrete examples to parts of a program to receive continuous, up-to-date feedback as their program unfolds. To reduce the manual effort involved in example construction, recent approaches either reuse run-time data mined from previous executions or construct synthetic inputs. Reusing observed examples lacks control over their content, whereas synthetic input does not yet scale to larger domain models. Our approach extends ELP with user-configurable, generated examples that scale to complex object graphs. In contrast to previous generation strategies using large language models (LLMs) with static context, we let an LLM guide the exploration of a code base to construct the required context and validate and refine proposed examples using execution feedback. We evaluated our example-generation agent on a synthetic dataset of 12 programs with varying complexity, and validated it on 4 real-world projects, demonstrating that the vast majority of functions and branches can be reached through a generated example. We found that execution feedback enabled smaller, locally hosted models to reach the performance of frontier models, while numeric and formal reasoning remained a consistent weakness across LLMs. We further developed a prototype that integrates our example-generation agent into an ELP system in Visual Studio Code. Our exploratory intra-subject study (n = 8) using program comprehension tasks, comparing our prototype to GitHub Copilot as the baseline, revealed that participants trusted their acquired knowledge more when ad-hoc examples were available and used the tool like a lightweight debugger, while Copilot was perceived as providing more accessible, but less reliable predictions rather than execution-grounded observations. However, we found no effect on the correctness of answers to program comprehension questions. In connection with existing ELP systems and AI assistants, automating example generation can achieve ubiquitous run-time feedback available to both programmers and AI. |
|
| Krishnamurthi, Shriram |
Shriram Krishnamurthi and Matthew Flatt (Brown University, USA; University of Utah, USA) Context For decades, programming language implementors have designed error messages with one consumer in mind: the human programmer. Human-factors research has consistently found that programmers engage with error messages poorly—they skim, miss key information, and are easily overwhelmed. A practical consequence has been a strong design pressure toward brevity so that programmers will actually read them. Inquiry AI coding agents are now a second consumer of error messages. Unlike humans, agents will read large quantities of prose; the only practical limit on message size is the context window, and modern context windows are large. This raises a question the programming-language community has not previously had reason to ask: should error-message detail be calibrated differently for AI agents than for humans? Approach We investigate this question through a controlled experiment using Shplait, an ML-style statically typed language. We construct a suite of programs containing a single deliberate type error each, and measure how often an AI agent repairs them under ablation: a detailed error context; a proximate error location; a minimal type error; and a dynamic (test suite) error only. An automated oracle uses a combination of a type checker and a test suite to classify each modified program as having a type error, being type-correct but semantically incorrect, or being semantically correct. Knowledge We find concrete evidence that more detailed error messages generally improve an agent’s ability to fix type errors. We also see evidence that agents are able to fix programs whose names have all been obfuscated. Grounding Our primary experiment comprises 2,400 trials across ten complete runs, using both qwen2.5-coder:14b (a quality open-weight model) and claude-haiku-4.5 (a quality commercial model) via ollama and aider on dedicated GPU hardware. The experimental platform—correct programs, their erroneous counterparts, error modes, and oracle—is described in full. Importance If more detailed error messages genuinely help AI agents, then languages designed with only human readers in mind may be providing a suboptimal experience for AI coding. Our results suggest that it is worth considering offering two reporting modes: a terse human mode and a detailed AI mode. More broadly, we believe that language-model-targeted error-message design is an open and important design problem. |
|
| Mattis, Toni |
Toni Mattis, Benjamin Frost, Lukas Böhme, and Robert Hirschfeld (Hasso Plattner Institute, Germany; University of Potsdam, Germany) Programming often benefits from dynamic information that complements source code. In particular, program comprehension can take advantage of concrete run-time data whose structure and changes give meaning to abstract identifiers and computational steps. Obtaining up-to-date run-time information from a part of a system poses a number of challenges: First, a suitable entry point from which to run the code in question is needed. Second, such an entry point might require an explicit setup and expect specific input to reveal the behavior of interest. Third, execution should be repeatable to react immediately to code or input changes. In example-based live programming (ELP), programmers can attach concrete examples to parts of a program to receive continuous, up-to-date feedback as their program unfolds. To reduce the manual effort involved in example construction, recent approaches either reuse run-time data mined from previous executions or construct synthetic inputs. Reusing observed examples lacks control over their content, whereas synthetic input does not yet scale to larger domain models. Our approach extends ELP with user-configurable, generated examples that scale to complex object graphs. In contrast to previous generation strategies using large language models (LLMs) with static context, we let an LLM guide the exploration of a code base to construct the required context and validate and refine proposed examples using execution feedback. We evaluated our example-generation agent on a synthetic dataset of 12 programs with varying complexity, and validated it on 4 real-world projects, demonstrating that the vast majority of functions and branches can be reached through a generated example. We found that execution feedback enabled smaller, locally hosted models to reach the performance of frontier models, while numeric and formal reasoning remained a consistent weakness across LLMs. We further developed a prototype that integrates our example-generation agent into an ELP system in Visual Studio Code. Our exploratory intra-subject study (n = 8) using program comprehension tasks, comparing our prototype to GitHub Copilot as the baseline, revealed that participants trusted their acquired knowledge more when ad-hoc examples were available and used the tool like a lightweight debugger, while Copilot was perceived as providing more accessible, but less reliable predictions rather than execution-grounded observations. However, we found no effect on the correctness of answers to program comprehension questions. In connection with existing ELP systems and AI assistants, automating example generation can achieve ubiquitous run-time feedback available to both programmers and AI. |
|
| Weston, Olivia |
Olivia Weston and Simon Fowler (University of Glasgow, UK) Context Behavioural type systems such as session types, typestate, and mailbox types allow a developer to specify and check behavioural properties within their application code, giving programs that are correct-by-construction. Session types in particular allow a developer that communication in their code follows pre-defined protocols. Inquiry Implementing session types in functional languages requires some form of resource control, most commonly achieved through the use of linear typing. However, linear type systems as specified declaratively cannot be implemented algorithmically. Even when using techniques such as leftover typing, implementing other substructural modes (e.g., affine and relevant) requires ad-hoc changes to typing rules. Approach We investigate co-contextual type systems as a general framework for implementing substructural type systems. Whereas standard type systems require a type environment as an input to a typechecking algorithm, co-contextual type systems—a class of type system originally introduced for efficient incremental typechecking—produce a type environment as an output of the typechecking judgement. Knowledge We show how to generalise co-contextual type systems to support algorithmic implementations of substructural typing: simple changes to typechecker parameters allow us to instantiate our typechecker to check unrestricted, linear, affine, and relevant λ-calculi. Building on this approach, we present a second language with an extended constraint system that can support mixed-linearity typing, and we use this to implement an algorithmic type system for the GV session-typed functional language. Grounding We prove four instantiations of our algorithm sound and complete with respect to declarative unrestricted, linear, affine, and relevant λ-calculi. We prove our our co-contextual session typing algorithm sound and complete with respect to a declarative presentation of GV. Finally, we implement our typechecking algorithm in OCaml and demonstrate it on a series of case study applications. Importance This work shows the versatility of co-contextual typing as a framework for supporting algorithmic implementations of substructural type systems, in addition to its originally-presented benefits (e.g., support for incremental and parallel typechecking). Our work further lays the groundwork for implementing programming languages with more sophisticated type combination operations that are out-of-reach of current approaches. |
12 authors
proc time: 1.1