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. From Spatial Relations to Spatial Configurations

   Dan, Soham ; Kordjamshidi, Parisa ; Bonn, Julia ; Bhatia, Archna ; Cai, Jon ; Palmer, Martha ; Roth, Dan ( April 2020 , Proceedings of the 12th Conference on Language Resources and Evaluation (LREC 2020))

   Spatial Reasoning from language is essential for natural language understanding. Supporting it requires a representation scheme that can capture spatial phenomena encountered in language as well as in images and videos. Existing spatial representations are not sufficient for describing spatial configurations used in complex tasks. This paper extends the capabilities of existing spatial representation languages and increases coverage of the semantic aspects that are needed to ground spatial meaning of natural language text in the world. Our spatial relation language is able to represent a large, comprehensive set of spatial concepts crucial for reasoning and is designed to support composition of static and dynamic spatial configurations. We integrate this language with the Abstract Meaning Representation (AMR) annotation schema and present a corpus annotated by this extended AMR. To exhibit the applicability of our representation scheme, we annotate text taken from diverse datasets and show how we extend the capabilities of existing spatial representation languages with fine-grained decomposition of semantics and blend it seamlessly with AMRs of sentences and discourse representations as a whole. 

   more » « less
5. 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