More Like this

1. Indexed Streams: A Formal Intermediate Representation for Fused Contraction Programs

   https://doi.org/10.1145/3591268  

   Kovach, Scott; Kolichala, Praneeth; Gu, Tiancheng; Kjolstad, Fredrik (June 2023, Proceedings of the ACM on Programming Languages)

   We introduce indexed streams, a formal operational model and intermediate representation that describes the fused execution of a contraction language that encompasses both sparse tensor algebra and relational algebra. We prove that the indexed stream model is correct with respect to a functional semantics. We also develop a compiler for contraction expressions that uses indexed streams as an intermediate representation. The compiler is only 540 lines of code, but we show that its performance can match both the TACO compiler for sparse tensor algebra and the SQLite and DuckDB query processing libraries for relational algebra. 

   more » « less
2. A Formal Model of Checked C

   https://doi.org/10.1109/CSF54842.2022.9919657  

   Li, Liyi; Liu, Yiyun; Postol, Deena; Lampropoulos, Leonidas; Van Horn, David; Hicks, Michael (August 2022, 2022 IEEE 35th Computer Security Foundations Symposium (CSF))

   We present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potentially null-terminated arrays. We formalize this model in Coq, and prove that any spatial memory safety errors can be blamed on portions of the program labeled unchecked; this is a Checked C feature that supports incremental porting and backward compatibility. While our model's operational semantics uses annotated (“fat”) pointers to enforce spatial safety, we show that such annotations can be safely erased. Using PLT Redex we formalize an executable version of our model and a compilation procedure to an untyped C-like language, as well as use randomized testing to validate that generated code faithfully simulates the original. Finally, we develop a custom random generator for well-typed and almost-well-typed terms in our Redex model, and use it to search for inconsistencies between our model and the Clang Checked C implementation. We find these steps to be a useful way to co-develop a language (Checked C is still in development) and a core model of it. 

   more » « less
3. Semantics for Conditional Literals via the SM Operator

   https://doi.org/10.1007/978-3-031-15707-3_20  

   Hansen, Z.; Lierler, Y. (August 2022, Logic Programming and Nonmonotonic Reasoning)

   Conditional literals are an expressive Answer Set Programming language construct supported by the solver clingo. Their semantics are currently defined by a translation to infinitary propositional logic, however, we develop an alternative characterization with the SM operator which does not rely on grounding. This allows us to reason about the behavior of a broad class of clingo programs/encodings containing conditional literals, without referring to a particular input/instance of an encoding. We formalize the intuition that conditional literals behave as nested implications, and prove the equivalence of our semantics to those implemented by clingo. 

   more » « less
4. Respect the code: Speakers expect novel conventions to generalize within but not across social group boundaries

   Hawkins, Robert D.; Liu, I; Goldberg, Adele E.; Griffiths, Thomas L. (January 2021, Proceedings of the Annual Conference of the Cognitive Science Society)

   null (Ed.)

   Speakers use different language to communicate with partners in different communities. But how do we learn and represent which conventions to use with which partners? In this paper, we argue that solving this challenging computational problem requires speakers to supplement their lexical representations with knowledge of social group structure. We formalize this idea by extending a recent hierarchical Bayesian model of convention formation with an intermediate layer explicitly representing the latent communities each partner belongs to, and derive predictions about how conventions formed within a group ought to extend to new in-group and out-group members. We then present evidence from two behavioral experiments testing these predictions using a minimal group paradigm. Taken together, our findings provide a first step toward a formal framework for understanding the interplay between language use and social group knowledge. 

   more » « less
5. A Survey on Event-Based News Narrative Extraction

   https://doi.org/10.1145/3584741  

   Keith Norambuena, Brian Felipe; Mitra, Tanushree; North, Chris (December 2023, ACM Computing Surveys)

   Narratives are fundamental to our understanding of the world, providing us with a natural structure for knowledge representation over time. Computational narrative extraction is a subfield of artificial intelligence that makes heavy use of information retrieval and natural language processing techniques. Despite the importance of computational narrative extraction, relatively little scholarly work exists on synthesizing previous research and strategizing future research in the area. In particular, this article focuses on extracting news narratives from an event-centric perspective. Extracting narratives from news data has multiple applications in understanding the evolving information landscape. This survey presents an extensive study of research in the area of event-based news narrative extraction. In particular, we screened more than 900 articles, which yielded 54 relevant articles. These articles are synthesized and organized by representation model, extraction criteria, and evaluation approaches. Based on the reviewed studies, we identify recent trends, open challenges, and potential research lines. 

   more » « less