More Like this

1. Logical bytecode reduction

   https://doi.org/10.1145/3453483.3454091  

   Kalhauge, Christian Gram; Palsberg, Jens (June 2021, 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI))

   null (Ed.)

   Reducing a failure-inducing input to a smaller one is challenging for input with internal dependencies because most sub-inputs are invalid. Kalhauge and Palsberg made progress on this problem by mapping the task to a reduction problem for dependency graphs that avoids invalid inputs entirely. Their tool J-Reduce efficiently reduces Java bytecode to 24 percent of its original size, which made it the most effective tool until now. However, the output from their tool is often too large to be helpful in a bug report. In this paper, we show that more fine-grained modeling of dependencies leads to much more reduction. Specifically, we use propositional logic for specifying dependencies and we show how this works for Java bytecode. Once we have a propositional formula that specifies all valid sub-inputs, we run an algorithm that finds a small, valid, failure-inducing input. Our algorithm interleaves runs of the buggy program and calls to a procedure that finds a minimal satisfying assignment. Our experiments show that we can reduce Java bytecode to 4.6 percent of its original size, which is 5.3 times better than the 24.3 percent achieved by J-Reduce. The much smaller output is more suitable for bug reports. 

   more » « less
2. Inquiry and Logical Form

   https://doi.org/10.1111/phpe.70001  

   Stojnić, Una; Stone, Matthew (September 2025, Philosophical Perspectives)

   ABSTRACT Joint inquiry requires agents to exchange public content about some target domain, which in turn requires them to track which content a linguistic form contributes to a conversation. But, often, the inquiry delivers a necessary truth. For example, if we are inquiring whether a particular bird, Tweety, is a woodpecker, and discover that it is, then our inquiry concluding in this fact would conclude in a necessity, and the form “Tweety is a woodpecker” expresses this necessary truth. Still, whether Tweety is a woodpecker seems a perfectly legitimate object of study, and the answers we accrue can be informative. But the dominant model of inquiry (Stalnaker, 1978, 1984) treats this situation as linguistically deviant, and diagnoses our ignorance and subsequent discovery as metalinguistic: we were ignorant, and ultimately discovered something, about the meaning of our terms. Rather than linguistic deviation, we argue this situation is the norm, and one that calls for an alternative model of inquiry. This paper develops such a model. It shows that to capture how agents can learn something informative about the world—and not merely language—even when inquiry concerns necessary facts, it's key to track how moves in discourse contribute public content onto the conversational record, but also, crucially, how those moves are connected by coherence relations to one another and to real‐world situations they are about. This allows us to capture that utterances contribute determinate, public content, while representing the information states of the interlocutors who may have only partial access to the evidence and content of the conversation, without making their ignorance metalinguistic. It lets us give precise explanations why some discourses can be transparently convincing in the conclusions they underwrite. The model thus precisifies the role of public context and shared content in anchoring an inquiry. It allows for imperfect tracking of linguistic contributions that are binding for how inquiry unfolds, and it allows for an inquiry into the status of necessary truths to be both informative, and involve empirical, rather than metalinguistic, ignorance. 

   more » « less
3. The Logical Options Framework

   Brandon Araki, Xiao Li (July 2021, International Conference on Machine Learning)

   Learning composable policies for environments with complex rules and tasks is a challenging problem. We introduce a hierarchical reinforcement learning framework called the Logical Options Framework (LOF) that learns policies that are satisfying, optimal, and composable. LOF efficiently learns policies that satisfy tasks by representing the task as an automaton and integrating it into learning and planning. We provide and prove conditions under which LOF will learn satisfying, optimal policies. And lastly, we show how LOF’s learned policies can be composed to satisfy unseen tasks with only 10-50 retraining steps on our benchmarks. We evaluate LOF on four tasks in discrete and continuous domains, including a 3D pick-and-place environment. 

   more » « less
4. A cost-aware logical framework

   https://doi.org/10.1145/3498670  

   Niu, Yue; Sterling, Jonathan; Grodin, Harrison; Harper, Robert (January 2022, Proceedings of the ACM on Programming Languages)

   We present calf , a c ost- a ware l ogical f ramework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of programming languages in terms of a modal account of phase distinctions , we argue that the cost structure of programs motivates a phase distinction between intension and extension . Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. As a full-spectrum dependent type theory, calf presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available in type theoretic proof assistants. We evaluate calf as a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: the method of recurrence relations and physicist’s method for amortized analysis . We deploy these techniques on a variety of case studies: we prove a tight, closed bound for Euclid’s algorithm, verify the amortized complexity of batched queues, and derive tight, closed bounds for the sequential and parallel complexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning in calf by means of a model construction. 

   more » « less
5. Logical Aspects of Quantum Structures

   https://doi.org/10.1007/978-3-030-98689-6_6  

   Harding, J; Wang, Z (January 2022, Springer International Publishing)