Elpi is a higher-order logic programming language derived from λ Prolog and widely used to extend the Rocq interactive theorem prover. Typical users are familiar with types and functional programming but often lack experience with backtracking. We introduce a language of signatures to declare that a predicate is operationally deterministic, meaning that calling the predicate does not leave any choice points. The signature language handles higher-order programs and dynamic programs. We present a static analyzer that verifies these signatures and report its application to the majority of public Elpi code in the Rocq ecosystem.
Static program verification tools are essential for ensuring software correctness and reliability without executing the code. However, their effectiveness relies heavily on precise configuration, which must be tailored to specific project requirements, coding standards, and quality objectives. Selecting appropriate configurations is challenging due to the unique properties of each codebase and the need for an in-depth understanding of the analysis techniques. Current methods often default to standard settings or rely on random exploration, leading to sub-optimal results. In this paper, we introduce ConfigTuneX, a novel rule-based machine learning approach that optimizes configuration settings in static program verification tools through composite FOLD-SE rules. These rules simultaneously address two critical challenges: (1) reducing inconclusive outcomes by distinguishing unresolved cases from resolved outcomes, and (2) improving verification accuracy by separating correct outcomes from incorrect ones. The extracted rules are transformed into stratified answer set program (ASP) compatible with the s(CASP) solver, which systematically generates counterfactual configurations to avoid undesired outcomes. This targeted reasoning narrows the search space to the most promising configurations, reducing computational overhead while enhancing both interpretability and effectiveness. Experimental results show that ConfigTuneX with composite FOLD-SE rules consistently outperforms the state-of-the-art baseline across verification tools. On Jayhorn, CBMC, and Symbiotic, ConfigTuneX improves success rates by 76.34
Answer Set Programming with Quantifiers (ASP(Q)) extends classical ASP to naturally capture problems within the polynomial hierarchy (PH). Recently, the formalism has been enriched with weak constraints to express both local and global optimization criteria, enabling the modeling of problems in _n+1^P . In this paper, we present the first implementation of ASP(Q) with global weak constraints, built on top of the state-of-the-art ASP(Q) system PyQASP, based on an upper-bound improving strategy that effectively guides the search toward optimal solutions. Experiments demonstrate that our approach can be effectively applied to solve hard optimization problems.
Functional reactive programming (FRP) is a programming paradigm for implementing software that continuously interacts with its environment and manipulates highly dynamic data. Asynchronous FRP, in particular, is very expressive and can be used to implement graphical user interfaces and other reactive systems interacting with data streams and events that are not synchronized. Testing such asynchronous FRP programs is difficult since a program’s behaviour depends not only on the concrete data it receives from its environment but also the relative timing of when each piece of data arrives. In this paper, we propose PropRatt, a property-based testing framework for asynchronous FRP. The key component of PropRatt is its specification language, which extends basic linear temporal logic with a means to express properties of several concurrent signals. This allows us to express temporal properties that relate data coming from different signals at different points in time. PropRatt is implemented in Haskell and targets a recently introduced asynchronous FRP language embedded in Haskell. We demonstrate the utility of PropRatt through a case study testing a signal combinator library as well as a graphical user interface, in which we suggest how the strategy for generating signals can be modified to better model specific domains.
Various approaches to solving set theory constraints exist, for example within verification tools for the TLA+ and B formal methods. In this paper we present a way to solve set theory constraints in general and B formulas in particular using SAT solvers, by using Prolog technology. First, a preliminary analysis uses CLP(FD) constraint solving to infer finite bounds for decision variables. Second, Prolog translation rules map constraints to answer set programming (ASP), by encoding logical and set-theoretic operators as Horn clauses. Finally, the Clingo tool translates the ASP encoding to SAT to produce ASP models, which we translate back to set theory and B using Prolog DCG rules. The scheme of the paper has been implemented in SICStus Prolog, as an alternate backend for the ProB validation tool. We evaluate the new backend on a series of benchmarks. Our paper highlights the usefulness of Prolog, for analysis, inference and transformation rules and ASP as a high-level interface to SAT solving.
Solving textual reasoning problems by translating them into logic has proven effective, as it reduces hallucinations and allows the logic solver to handle complex reasoning. However, there is one major challenge that makes this technique difficult to apply to many practical reasoning problems. Arguments presented in text often have implicit rules that are assumed to be part of commonsense knowledge and are therefore omitted. They need to be identified and explicitly added to a logic program for accurate reasoning. This process is typically called argument reconstruction. Discovering these implicit logic rules is a challenging problem that previous text-to-logic translation systems struggle with. In this paper, we present a novel system that reconstructs these implicit rules in 3 stages: (i) Translating the problem from text to First Order Logic (FOL), (ii) Translating FOL to an equivalent s(CASP) answer set program that can compute gap predicates (predicates whose derivation requires implicit rules), and (iii) Using an LLM to generate required implicit rules for these gap predicates. We show that our system generates implicit rules to effectively solve reasoning problems drawn from a popular benchmark designed to be challenging for LLMs.
Prolog systems traditionally employ leftmost, depth-first search as their execution strategy. This choice is well-justified for efficiency reasons, generally accepted, and useful in practice. However, it is also well-known that it can lead to incompleteness when evaluating programs over infinite search spaces and may not be ideal for complex search spaces. We revisit the role of search strategies in Prolog programs, and present a new approach, that enables programmable and composable control of search. While advanced search strategies can always be programmed in Prolog, we opt instead for an approach that separates the search strategy used from the actual code, so that different strategies can be used on the same set of clauses. We provide constructs for controlling the search strategies that allow adapting the search dynamically. We also illustrate the usefulness of the proposed approach by applying it in the context of testing (constraint) logic programs, showing how composable search parameters enable more controlled and targeted exploration of program behavior.
Danvy Nielsen’s one-pass CPS transform has a straightforward definition, but clashes between the names of variables it introduces make it difficult to mechanically prove correct. Existing mechanical proofs either side-step the issue by using nameless representations, or rely on tedious α -equivalence relations between target terms. This paper presents a new formulation of the transform using evaluation contexts that allows deterministic introduction of fresh names, eliminating the need to work up to α -equivalence. We use our formulation to present a new and straightforward simulation proof of the correctness of the one-pass CPS transform, which we have mechanised in the HOL4 theorem prover.
Network troubleshooting today relies largely on ticket systems, which log, record, replay, and analyze live events, while overlooking recent advances in SDNs, programmable networks, and verified data centers, all of which have produced a rich body of models and control software. We argue instead that this modern network software—including abstract models and system code—provides a vantage point for troubleshooting, enabled by a debugger that, when things go bump in the night, allows someone who neither wrote the software nor is familiar with the DSL or verification tools to pinpoint the exact culprit line—a stepping stone for systematically diagnosing the underlying network. As a first step toward this vision, we present a declarative debugging schema for modern network software amid its rapid evolution: the user only needs to answer “yes/no” questions about the software’s intended behavior, leaving procedural inspection and bug localization entirely to the debugger; meanwhile, new language features—arisen with emerging applications—are seamlessly supported through a novel use of partial evaluation, which automatically incorporates these features into the declarative debugging process.
Knowledge base systems (KBS) store declarative knowledge, on which they can execute different inference tasks, such as “propagation”, which is the derivation of consequences of some given information with respect to the knowledge base. When building larger applications that make use of such a KBS, specific inference tasks are typically invoked through an imperative API. For instance, both the Clasp system for Answer Set Solving and the IDP-Z3 reasoning engine for the FO( · ) language offer a Python API for this. However, when the application should be deployed, e.g., in the cloud or on embedded hardware, it is not always convenient or even possible to include the entire KBS as a separate component. For this reason, we investigate the compilation of a knowledge base into a Python program that can perform propagation inference without needing access to an external solver. We investigate this approach for the FO( · ) language, presenting and comparing two compilation methods. Experimental results on these two methods demonstrate that high-level propagators achieve better performance than grounded propagators.
Parsing is one of the foundational problems in the field of programming languages. While the theory of parsing with context free grammars is well understood, parsing more complex languages remains a hard problem. Indentation-sensitive languages are an important subset of languages that have been studied extensively. We build on both Adams’ work of indentation-sensitive parsing and Caballero et al.’s work on functional logic parsing to show how functional logic languages can elegantly solve the problem of indentation-sensitive parsing.
Systematic discovery of optimization paths in quantum circuit simplification remains a challenge. Today, ZX-calculus, a computing model for quantum circuit transformation, is attracting attention for its highly abstract graph-based approach. Whereas existing tools such as PyZX and Quantomatic offer domain-specific support for quantum circuit optimization, visualization and theorem-proving, we present a complementary approach using LMNtal, a general-purpose hierarchical graph rewriting language, to establish a diagrammatic transformation and verification platform with model checking. Our methodology shows three advantages: (1) a direct and concise encoding of the ZX-calculus, where quantifiers simplify complex rule specification; (2) a verification framework using state-space exploration and model checking to analyze rewrite strategies; and (3) an open platform for strategic experimentation combining programmable syntax with interactive visualization. Through case studies, we demonstrate how our framework helps understand optimization paths and design new algorithms and strategies. This suggests that the declarative language LMNtal and its toolchain could serve as a new platform to investigate quantum circuit transformation from a different perspective.
Parametricity and free theorems are a powerful tool for proving the correctness of optimizations. There has been some investigation of incorporating free theorems for functional logic languages, including a proof of the parametricity theorem for a sub-language of Curry. In this paper we explore the consequences of adding one optimization, shortcut deforestation, to a Curry compiler. We describe the optimization and give a proof of correctness. While proving the correctness of the optimization, we explore the application of parametricity and free theorems to Curry. This leads to some of the more surprising aspects of functional logic programming.
Heterogeneously typed sequences are supported in a wide range of programming languages, both dynamically and statically typed. These sequences often exhibit type patterns such as repetition, alternation, and optionality. The programmer needs a mechanism to declare and query adherence to this regularity. The theory of finite automata over finite alphabets was conceived for characterizing patterns in so-called regular languages, but does not exactly meet this challenge, because the set of potential elements of the sequences is infinite. In this article, we present a generalization of regular expressions called rational type expressions as a means of declaring regular patterns in heterogeneous sequences. We present procedures for constructing and manipulating symbolic finite automata, a generalization of classical finite automata, using a portable, simple, embeddable, type system. For type systems with subtyping, the subtype relation and type vacuity cannot always be computed programmatically. We provide a working, sound solution for constructing finite automata for type-based regular expressions even in cases where the subtype decidability relations is not computable retrospectively, but can be ensured by construction. We demonstrate the generality and portability of the system by providing implementations in Common Lisp, Clojure, Scala, and Python.
Spreadsheet programs are one of the most widespread information processing tools used by end-users. Their importance lies not only in their extensive use by people with little or no knowledge of programming but because of their relevance as a decision-making tool by executives in many companies. In spite of this long-term success, many studies have found plenty of pitfalls that make spreadsheets widely faulty, hence potentially leading to risky decisions. Because of these problems several analysis tools have been proposed to help find errors easily. In this project we present a different approach, more oriented to prevent the appearance of errors through a change in the way users interact with them. We focus on the declarative essence of spreadsheets and propose to refound them on the grounds of modern functional programming languages. Our tool uses a subset of Haskell as the expression language for its cells and takes advantage of its rich type system to support a safer way of spreadsheet programming that prevents the appearance of certain errors and helps to understand the meaning of programs, as new data types can be introduced from cell aggregates. Haskell is also used for defining reusable, user-defined functions and external modules. We show a working prototype incorporating the ideas above and point towards new features based on advanced functional programming technologies.
Machine learning models that automate decision-making are increasingly being used in consequential areas such as loan approvals, pretrial bail approval, hiring, and many more. Unfortunately, most of these models are black-boxes, i.e., they are unable to reveal how they reach these prediction decisions. A need for transparency demands justification for such predictions. An affected individual might also desire explanations to understand why a decision was made. Ethical and legal considerations may require informing individuals of changes needed to produce a desirable outcome. This paper focuses on this problem through the automatic generation of counterfactual explanations. We propose a framework Causally Constrained Counterfactual Generation (C3G) that utilizes Answer Set Programming (ASP) and the s(CASP) goal-directed ASP system to automatically generate counterfactual explanations from rules generated by rule-based machine learning (RBML) algorithms. Unlike traditional causal based approaches such as MINT, which relies on Structural Causal Models (SCMs) with predefined structural equations, C3G leverages the flexibility of Answer Set Programming (ASP) to model causal dependencies through logical rules, allowing for broader applicability across various domains. In our framework, we show how counterfactual explanations are computed and justified by imagining worlds where some or all factual assumptions are altered/changed. More importantly, we show how we can navigate between these worlds, namely, go from our original world/scenario where we obtain an undesired/negative outcome to the imagined world where we obtain a desired/positive outcome.
Runtime verification (RV) is a formal monitoring technique that uses formal specifications to create monitors. Stream runtime verification (SRV) extends RV from Boolean observations and verdicts to diverse data, allowing much richer monitors. This expressivity is challenging for developers of monitoring engines, so SRV tools end up fixing a collection of data theories for an application domain, and require significant overhead to incorporate new datatypes. Recent results allow incorporating Haskell datatypes transparently into generic SRV engines through the use of an embedded DSL, but the resulting syntax is conditioned by Haskell, every new monitor requires recompilation and error reporting is cryptic. In this paper, we introduce Mola, a generic implementation of an SRV engine that uses reflection in Haskell to implement a universal interpreter that offers data-theory extensibility and type guarantees as well as a simple syntax with useful error reports. Mola introduces the role of data-theory engineer, who easily defines datatypes for each application domain and compiles Mola into a specialized engine. The resulting tool is then used by specification engineers who define monitors that the engine can evaluate without recompilation. Hence, Mola finally realizes the promise of SRV to provide a clean separation between datatypes and temporal engines.
Modern answer set programming solvers such as CLINGO support advanced language constructs that improve the expressivity and conciseness of logic programs. Conditional literals are one such construct. They form "subformulas" that behave as nested implications within the bodies of logic rules. Their inclusion brings the form of rules closer to the less restrictive syntax of first-order logic. These qualities make conditional literals useful tools for knowledge representation. In this paper, we propose a semantics for logic programs with conditional literals and arithmetic based on the SM operator. These semantics do not require grounding, unlike the established semantics for such programs that relies on a translation to infinitary propositional logic. The main result of this paper establishes the precise correspondence between the proposed and existing semantics.
Prolog is a programming language that provides a high-level approach to software development. Python is a versatile programming language that has a vast range of libraries including support for data analysis and machine learning tasks. We present a Prolog-Python interface that aims at exploiting Prolog deduction capabilities and Python's extensive libraries. Our novel interface was built using a divide and conquer methodology. In a first step, we implemented a set of C++ classes that can be matched to Python classes; next, we used an interface generator to export the relevant classes. Finally, we use C code to actually convert between the two realms. In order to demonstrate the usefulness of the interface, we enhance an Inductive Logic Programming System with a visualization capabilities and show how to interface with a standard classifier.
This paper presents a practical application of Answer Set Programming (ASP) in the field of Language Documentation and Reclamation (LDR). LDR involves the systematic recording, preservation, analysis, and revitalization of endangered or dormant languages to protect linguistic diversity and cultural heritage. In collaboration with linguists working on the Myaamia language, we developed a derivational stemming tool that decomposes stems into their smallest meaningful units called morphemes. We explored different solvers and representations of stems and morphemes to identify the most efficient approach for several language documentation and research tasks. The tool’s accuracy was assessed by comparing its output with the stem decompositions documented in the ILDA database for Myaamia. The stemming tool for Myaamia–a reawakening Algonquian language with a growing number of second-language speakers–can serve as a model for stemming tools that can be adapted for other Algonquian languages based on the methods detailed in this paper.
