bluuebunny/crossref_metadata_2025 huggingface dataset:
Qualifying System F<:: Some Terms and Conditions May Apply
Authors: Lee Edward , Zhao Yaoyu , Lhoták Ondřej , You James , Satheeskumar Kavin , Brachthäuser Jonathan Immanuel
Published: April 2024

Type qualifiers offer a lightweight mechanism for enriching existing type systems to enforce additional, desirable, program invariants. They do so by offering a restricted but effective form of subtyping. While the theory of type qualifiers is well understood and present in many programming languages today, polymorphism over type qualifiers remains an area less well examined. We explore how such a polymorphic system could arise by constructing a calculus, System F-sub-Q, which combines the higher-rank bounded polymorphism of System F-sub with the theory of type qualifiers. We explore how the ideas used to construct System F-sub-Q can be reused in situations where type qualifiers naturally arise---in reference immutability, function colouring, and capture checking. Finally, we re-examine other qualifier systems in the literature in light of the observations presented while developing System F-sub-Q.
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
Authors: Cutler Joseph W. , Disselkoen Craig , Eline Aaron , He Shaobo , Headley Kyle , Hicks Michael , Hietala Kesha , Ioannidis Eleftherios , Kastner John , Mamat Anwar , McAdams Darin , McCutchen Matt , Rungta Neha , Torlak Emina , Wells Andrew M.
Published: April 2024

Cedar is a new authorization policy language designed to be ergonomic, fast, safe, and analyzable. Rather than embed authorization logic in an application’s code, developers can write that logic as Cedar policies and delegate access decisions to Cedar’s evaluation engine. Cedar’s simple and intuitive syntax supports common authorization use-cases with readable policies, naturally leveraging concepts from role-based, attribute-based, and relation-based access control models. Cedar’s policy structure enables access requests to be decided quickly. Cedar’s policy validator leverages optional typing to help policy writers avoid mistakes, but not get in their way. Cedar’s design has been finely balanced to allow for a sound and complete logical encoding, which enables precise policy analysis, e.g., to ensure that when refactoring a set of policies, the authorized
permissions do not change. We have modeled Cedar in the Lean programming language, and used Lean’s proof assistant to prove important properties of Cedar’s design. We have implemented Cedar in Rust, and released it open-source. Comparing Cedar to two open-source languages, OpenFGA and Rego, we find (subjectively) that Cedar has equally or more readable policies, but (objectively) performs far better.
Persimmon: Nested Family Polymorphism with Extensible Variant Types
Authors: Kravchuk-Kirilyuk Anastasiya , Feng Gary , Iskander Jonas , Zhang Yizhou , Amin Nada
Published: April 2024

Many obstacles stand in the way of modular, extensible code. Some language constructs, such as pattern matching, are not easily extensible. Inherited code may not be type safe in the presence of extended types. The burden of setting up design patterns can discourage users, and parameter clutter can make the code less readable. Given these challenges, it is no wonder that extensibility often gives way to code duplication. We present our solution: Persimmon, a functional system with nested family polymorphism, extensible variant types, and extensible pattern matching. Most constructs in our language are built-in "extensibility hooks," cutting down on the parameter clutter and user burden associated with extensible code. Persimmon preserves the relationships between nested families upon inheritance, enabling extensibility at a large scale. Since nested family polymorphism can express composable extensions, Persimmon supports mixins via an encoding. We show how Persimmon can be compiled into a functional language without extensible variants with our translation to Scala. Finally, we show that our system is sound by proving the properties of progress and preservation.
Gradually Typed Languages Should Be Vigilant!
Authors: Gierczak Olek , Menon Lucy , Dimoulas Christos , Ahmed Amal
Published: April 2024

In gradual typing, different languages perform different dynamic type checks for the same program even
though the languages have the same static type system. This raises the question of whether, given a gradually
typed language, the combination of the translation that injects checks in well-typed terms and the dynamic
semantics that determines their behavior sufficiently enforce the static type system of the language. Neither
type soundness, nor complete monitoring, nor any other meta-theoretic property of gradually typed languages
to date provides a satisfying answer.

In response, we present vigilance, a semantic analytical instrument that defines when the check-injecting
translation and dynamic semantics of a gradually typed language are adequate for its static type system.
Technically, vigilance asks if a given translation-and-semantics combination enforces the complete run-time
typing history of a value, which consists of all of the types associated with the value. We show that the standard
combination for so-called Natural gradual typing is vigilant for the standard simple type system, but the
standard combination for Transient gradual typing is not. At the same time, the standard combination for
Transient is vigilant for a tag type system but the standard combination for Natural is not. Hence, we clarify
the comparative type-level reasoning power between the two most studied approaches to sound gradual typing.
Furthermore, as an exercise that demonstrates how vigilance can guide design, we introduce and examine
a new theoretical static gradual type system, dubbed truer, that is stronger than tag typing and more faithfully
reflects the type-level reasoning power that the dynamic semantics of Transient gradual typing can guarantee.
Learning Abstraction Selection for Bayesian Program Analysis
Authors: Zhang Yifan , Shi Yuanfeng , Zhang Xin
Published: April 2024

We propose a learning-based approach to select abstractions for Bayesian program analysis. Bayesian program analysis converts a program analysis into a Bayesian model by attaching probabilities to analysis rules. It computes probabilities of analysis results and can update them by learning from user feedback, test runs, and other information. Its abstraction heavily affects how well it learns from such information. There exists a long line of works in selecting abstractions for conventional program analysis but they are not effective for Bayesian program analysis. This is because they do not optimize for generalization ability. We propose a data-driven framework to solve this problem by learning from labeled programs. Starting from an abstraction, it decides how to change the abstraction based on analysis derivations. To be general, it considers graph properties of analysis derivations; to be effective, it considers the derivations before and after changing the abstraction. We demonstrate the effectiveness of our approach using a datarace analysis and a thread-escape analysis.
Verification of Neural Networks’ Global Robustness
Authors: Kabaha Anan , Cohen Dana Drachsler
Published: April 2024

Neural networks are successful in various applications but are also susceptible to adversarial attacks. To show the safety of network classifiers, many verifiers have been introduced to reason about the local robustness of a given input to a given perturbation. While successful, local robustness cannot generalize to unseen inputs. Several works analyze global robustness properties, however, neither can provide a precise guarantee about the cases where a network classifier does not change its classification. In this work, we propose a new global robustness property for classifiers aiming at finding the minimal globally robust bound, which naturally extends the popular local robustness property for classifiers. We introduce VHAGaR, an anytime verifier for computing this bound. VHAGaR relies on three main ideas: encoding the problem as a mixed-integer programming and pruning the search space by identifying dependencies stemming from the perturbation or the network's computation and generalizing adversarial attacks to unknown inputs. We evaluate VHAGaR on several datasets and classifiers and show that, given a three hour timeout, the average gap between the lower and upper bound on the minimal globally robust bound computed by VHAGaR is 1.9, while the gap of an existing global robustness verifier is 154.7. Moreover, VHAGaR is 130.6x faster than this verifier. Our results further indicate that leveraging dependencies and adversarial attacks makes VHAGaR 78.6x faster.
A Pure Demand Operational Semantics with Applications to Program Analysis
Authors: Smith Scott , Zhang Robert
Published: April 2024

This paper develops a novel minimal-state operational semantics for higher-order functional languages that uses
only
the call stack and a source program point or a lexical level as the
complete
state information: there is no environment, no substitution, no continuation, etc. We prove this form of operational semantics equivalent to standard presentations.

We then show how this approach can open the door to potential new applications: we define a program analysis as a direct finitization of this operational semantics. The program analysis that naturally emerges has a number of novel and interesting properties compared to standard program analyses for higher-order programs: for example, it can infer recurrences and does not need value widening. We both give a formal definition of the analysis and describe our current implementation.
Degrees of Separation: A Flexible Type System for Safe Concurrency
Authors: Xu Yichen , Boruch-Gruszecki Aleksander , Odersky Martin
Published: April 2024

Data races have long been a notorious problem in concurrent programming. They are hard to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress has been made in this area, and these type systems are increasingly usable and practical. However, their adoption in mainstream programming languages is still limited, which is largely attributed to their strict alias prevention principles that obstruct the usage of existing programming patterns. This is a deterrent to the migration of existing code bases. To tackle this problem, we propose Capture Separation Calculus (System CSC), a calculus that models fork-join parallelism and statically prevents data races while being compatible with established programming patterns. It follows a
control-as-you-need
philosophy: by default, aliases are allowed, but they are tracked in the type system. When data races are a concern, the tracked aliases are controlled to prevent data-race-prone patterns. We study the formal properties of System CSC. Type soundness is proven via the standard progress and preservation theorems. Additionally, we formally verify the data race freedom property of System CSC by proving that the reduction of a well-typed program is confluent.
ParDiff: Practical Static Differential Analysis of Network Protocol Parsers
Authors: Zheng Mingwei , Shi Qingkai , Liu Xuwei , Xu Xiangzhe , Yu Le , Liu Congyu , Wei Guannan , Zhang Xiangyu
Published: April 2024

Countless devices all over the world are connected by networks and communicated via network protocols. Just like common software, protocol implementations suffer from bugs, many of which only cause silent data corruption instead of crashes. Hence, existing automated bug-finding techniques focused on memory safety, such as fuzzing, can hardly detect them. In this work, we propose a static differential analysis called ParDiff to find protocol implementation bugs, especially silent ones hidden in message parsers. Our key observation is that a network protocol often has multiple implementations and any semantic discrepancy between them may indicate bugs. However, different implementations are often written in disparate styles, e.g., using different data structures or written with different control structures, making it challenging to directly compare two implementations of even the same protocol. To exploit this observation and effectively compare multiple protocol implementations, ParDiff (1) automatically extracts finite state machines from programs to represent protocol format specifications, and (2) then leverages bisimulation and SMT solvers to find fine-grained and
semantic inconsistencies between them. We have extensively evaluated ParDiff using 14 network protocols. The results show that ParDiff outperforms both differential symbolic execution and differential fuzzing tools. To date, we have detected 41 bugs with 25 confirmed by developers.
A Constraint Solving Approach to Parikh Images of Regular Languages
Authors: Stjerna Amanda , Rümmer Philipp
Published: April 2024

A common problem in string constraint solvers is computing the Parikh image, a linear arithmetic formula that describes all possible combinations of character counts in strings of a given language. Automata-based string solvers frequently need to compute the Parikh image of products (or intersections) of finite-state automata, in particular when solving string constraints that also include the integer data-type due to operations like string length and indexing. In this context, the computation of Parikh images often turns out to be both prohibitively slow and memory-intensive. This paper contributes a new understanding of how the reasoning about Parikh images can be cast as a constraint solving problem, and questions about Parikh images be answered without explicitly computing the product automaton or the exact Parikh image. The paper shows how this formulation can be efficiently implemented as a calculus, PC*, embedded in an automated theorem prover supporting Presburger logic. The resulting standalone tool Catra is evaluate on constraints produced by the Ostrich+ string solver when solving standard string constraint benchmarks involving integer operations. The experiments show that PC* strictly outperforms the standard approach by Verma et al. to extract Parikh images from finite-state automata, as well as the over-approximating method recently described by Janků and Turoňová by a wide margin, and for realistic timeouts (under 60 s) also the nuXmv model checker. When added as the Parikh image backend of Ostrich+ to the Ostrich string constraint solver’s portfolio, it boosts its results on the quantifier-free strings with linear integer algebra track of SMT-COMP 2023 (QF_SLIA) enough to solve the most Unsat instances in that track of all competitors.
Scenario-Based Proofs for Concurrent Objects
Authors: Enea Constantin , Koskinen Eric
Published: April 2024

Concurrent objects form the foundation of many applications that exploit multicore architectures and their importance has lead to informal correctness arguments, as well as formal proof systems. Correctness arguments (as found in the distributed computing literature) give intuitive descriptions of a few canonical executions or "scenarios" often each with only a few threads, yet it remains unknown as to whether these intuitive arguments have a formal grounding and extend to arbitrary interleavings over unboundedly many threads.

We present a novel proof technique for concurrent objects, based around identifying a small set of scenarios (representative, canonical interleavings), formalized as the commutativity quotient of a concurrent object. We next give an expression language for defining abstractions of the quotient in the form of regular or context-free languages that enable simple proofs of linearizability. These quotient expressions organize unbounded interleavings into a form more amenable to reasoning and make explicit the relationship between implementation-level contention/interference and ADT-level transitions.

We evaluate our work on numerous non-trivial concurrent objects from the literature (including the Michael-Scott queue, Elimination stack, SLS reservation queue, RDCSS and Herlihy-Wing queue). We show that quotients capture the diverse features/complexities of these algorithms, can be used even when linearization points are not straight-forward, correspond to original authors' correctness arguments, and provide some new scenario-based arguments. Finally, we show that discovery of some object's quotients reduces to two-thread reasoning and give an implementation that can derive candidate quotients expressions from source code.
Mechanizing the CMP Abstraction for Parameterized Verification
Authors: Li Yongjian , Zhan Bohua , Pang Jun
Published: April 2024

Parameterized verification is a challenging problem that is known to be undecidable in the general case.  ‍is a widely-used method for parameterized verification, originally proposed by Chou, Mannava and Park in 2004. It involves abstracting the protocol to a small fixed number of nodes, and strengthening by auxiliary invariants to refine the abstraction. In most of the existing applications of CMP, the abstraction and strengthening procedures are carried out manually, which can be tedious and error-prone. Existing theoretical justification of the  ‍method is also done at a high level, without detailed descriptions of abstraction and strengthening rules. In this paper, we present a formally verified theory of  ‍in Isabelle/HOL, with detailed, syntax-directed procedure for abstraction and strengthening that is proven correct. The formalization also includes correctness of symmetry reduction and assume-guarantee reasoning. We also describe a tool AutoCMP for automatically carrying out abstraction and strengthening in , as well as generating Isabelle proof scripts showing their correctness. We applied the tool to a number of parameterized protocols, and discovered some inaccuracies in previous manual applications of  ‍to the FLASH cache coherence protocol.
Understanding and Finding Java Decompiler Bugs
Authors: Lu Yifei , Hou Weidong , Pan Minxue , Li Xuandong , Su Zhendong
Published: April 2024

Java decompilers are programs that perform the reverse process of Java compilers, i.e., they translate Java bytecode to Java source code. They are essential for reverse engineering purposes and have become more sophisticated and reliable over the years. However, it remains challenging for modern Java decompilers to reliably perform correct decompilation on real-world programs. To shed light on the key challenges of Java decompilation, this paper provides the first systematic study on the characteristics and causes of bugs in mature, widely-used Java decompilers. We conduct the study by investigating 333 unique bugs from three popular Java decompilers. Our key findings and observations include: (1) Although most of the reported bugs were found when decompiling large, real-world code, 40.2% of them have small test cases for bug reproduction; (2) Over 80% of the bugs manifest as exceptions, syntactic errors, or semantic errors, and bugs with source code artifacts are very likely semantic errors; (3) 57.7%, 39.0%, and 41.1% of the bugs respectively are attributed to three stages of decompilers—loading structure entities from bytecode, optimizing these entities, and generating source code from these entities; (4) Bugs in decompilers’ type inference are the most complex to fix; and (5) Region restoration for structures like loop, sugaring for special structures like switch, and type inference of variables of generic types or indistinguishable types are the three most significant challenges in Java decompilation, which to some extent explains our findings in (3) and (4).

Based on these findings, we present JD-Tester, a differential testing framework for Java decompilers, and our experience of using it in testing the three popular Java decompilers. JD-Testerutilizes different Java program generators to construct
executable
Java tests and finds exceptions, syntactic, and semantic inconsistencies (i.e. bugs) between a generated test and its
compiled-decompiled
version (through compilation and execution). In total, we have found 62 bugs in the three decompilers, demonstrating both the effectiveness of JD-Tester, and the importance of testing and validating Java decompilers.
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
Authors: Ye Qianchuan , Delaware Benjamin
Published: April 2024

Secure multiparty computation (MPC) techniques enable multiple parties to compute joint functions over their private data without sharing that data with other parties, typically by employing powerful cryptographic protocols to protect individual's data. One challenge when writing such functions is that most MPC languages force users to intermix programmatic and privacy concerns in a single application, making it difficult to change or audit a program's underlying privacy policy. Prior policy-agnostic MPC languages relied on dynamic enforcement to decouple privacy requirements from program logic. Unfortunately, the resulting overhead makes it difficult to scale MPC applications that manipulate structured data. This work proposes to eliminate this overhead by instead transforming programs into semantically equivalent versions that statically enforce user-provided privacy policies. We have implemented this approach in a new MPC language, called Taypsi; our experimental evaluation demonstrates that the resulting system features considerable performance improvements on a variety of MPC applications involving structured data and complex privacy policies.
Modeling Dynamic (De)Allocations of Local Memory for Translation Validation
Authors: Rose Abhishek , Bansal Sorav
Published: April 2024

End-to-End Translation Validation is the problem of verifying the executable code generated by a compiler against the corresponding input source code for a single compilation. This becomes particularly hard in the presence of dynamically-allocated local memory where addresses of local memory may be observed by the program. In the context of validating the translation of a C procedure to executable code, a validator needs to tackle constant-length local arrays, address-taken local variables, address-taken formal parameters, variable-length local arrays, procedure-call arguments (including variadic arguments), and the
alloca
() operator. We provide an execution model, a definition of refinement, and an algorithm to soundly convert a refinement check into first-order logic queries that an off-the-shelf SMT solver can handle efficiently. In our experiments, we perform blackbox translation validation of C procedures (with up to 100+ SLOC), involving these local memory allocation constructs, against their corresponding assembly implementations (with up to 200+ instructions) generated by an optimizing compiler with complex loop and vectorizing transformations.
CRAYON: Exploration on Community-based Relayed Online Education Approach for Rural Children in South Korean EFL Context
Authors: Kim Seonghoon , Lee Hyunjong , Kang Seongwoong , Goh Michelle , Kim Wonjung , Lee Seungchul , Park Souneil , Ahn So-Yeon , Song Junehwa
Published: April 2024

Rural children in South Korea exhibit higher foreign language anxiety and lower English competency. For such marginalized contexts where local communities cannot support children's learning, we propose and explore a new pedagogical approach, CRAYON (Community-based RelAY Online educatioN). In CRAYON, a pool of non-professional tutors take turns to meet and teach rural children in short relay sessions through mobile technologies. It uncovers and promotes volunteers' internal willingness to participate in community-based teaching, which could otherwise be fragmented and dormant in their tightly-woven daily lives. It greatly lessens the barriers to participation from multiple dimensions, i.e., time, space, and expertise, and encourages interested volunteers to easily join without taking much burden. As such, the approach can create new learning opportunities and help rural children overcome their motivational and environmental hurdles. Tutors could approach each child and share short but precious time with her; helping her experience repetitive and sufficient exposure to the language, each time with a newly met tutor. We conducted a short relay session-based English learning program for 5 rural children for 4 weeks in South Korea with 15 tutors. From the field deployment, we find that the rural children and the undergraduate tutors engaged in effective interactions and scaffolding, despite the constraints of partitioned short sessions. A particular pattern of interaction, i.e., continuous learner engagement support, emerged as they drew out the interactions over a short period of time. It was highly encouraging to observe that all children, including those who were disengaged in their classroom environments, actively participated in the CRAYON sessions. The findings elicited from the study have important implications in multiple dimensions. They suggest the possibility of extending the scope of learning environments to include first-met tutors and learners beyond re-established relationship. In a larger perspective, the findings imply a new direction to overcome the challenges of low childhood literacy in under-resourced areas. With adequate and sufficient support from educational institutions and CRAYON, this study argues that volunteer tutors with less experience can deliver effective instruction by sharing just a short period of time, and help a child who has been lagging behind the pace of the school catch up and re-engage.
Experiences from Running a Participatory Media Platform for Women and Led by Women in Rural North India
Authors: Chakraborty Dipanjan , Chatterjee Sayonee , Tripathi Rajeshwari , Gupta Akshay , Seth Aaditeshwar
Published: April 2024

Patriarchal practices and other socio-cultural norms in rural North India often prevent women from participating in digital platforms. In this paper we present a voice-based participatory community media platform that runs over simple voice-based phone calls. The platform is meant for women users and is led by women and has been used by 12,222 women users over the course of 20 months. We conduct a qualitative study and present several innovations, such as creating a safe space for women, which have contributed to more participation of women on the platform. We present a framework which can serve as a guidance for researchers and practitioners who want to set up digital platforms for women users.
Dismantling Gender Blindness in Online Discussion of a Crime/Gender Dichotomy
Authors: Qin Yigang , Duan Weilun , Wu Qunfang , Lu Zhicong
Published: April 2024

Contemporary feminists utilize social media for activism, while backlashes come along. The gender-related discourses are often diminished when addressing public events regarding sexism and gender inequality on social media platforms. The dichotomous debate around the Tangshan beating incident in China epitomized how criminal interpretations of gender-related violence became a backlash against feminist expressions. By analyzing posts on Weibo using mixed methods, we describe the emerging discursive patterns around crime and gender, uncovering the gender-blind sexism that refutes feminist discourses on the social platform. We also highlight the critical hurdles facing grassroots feminist activism in Chinese cyberspace and propose implications for the design and research related to digital feminist activism.
Delivering the Future: Understanding User Perceptions of Delivery Robots
Authors: Shin Hyorim , Choi Junho , Oh Changhoon
Published: April 2024

Delivery robots are increasingly becoming part of our urban landscape. However, the general public is divided about their presence in public spaces; some welcome their usefulness, while others see them as intrusive or even threatening. This study aims to understand users' perceptions of these robots to provide concrete insights into their further development. First, we used text mining to analyze people's reactions to popular YouTube videos featuring delivery robots. Based on these findings, we applied the scenario-based design method to develop scenarios illustrating user interactions with delivery robots. We then conducted in-depth interviews with 30 participants to explore their views on these scenarios. Our analysis highlighted several design issues, including robots' aesthetics, interactions with pedestrians, and the broader physical and regulatory framework. We also identified common concerns and positive expectations for these robots. From these findings, we propose design implications for the future of delivery robots.
Understanding Multi-user, Handheld Mixed Reality for Group-based MR Games
Authors: Bautista Isaza Carlos Augusto , Enriquez Daniel , Moon Hayoun , Jeon Myounghoon , Lee Sang Won
Published: April 2024

Research has identified applications of handheld-based VR, which utilizes handheld displays or mobile devices, for developing systems that involve users in mixed reality (MR) without the need for head-worn displays (HWDs). Such systems can potentially accommodate large groups of users participating in MR. However, we lack an understanding of how group sizes and interaction methods affect the user experience. In this paper, we aim to advance our understanding of handheld-based MR in the context of multiplayer, co-located games. We conducted a study (N = 38) to understand how user experiences vary by group size (2, 4, and 8) and interaction method (proximity-based or pointing-based). For our experiment, we implemented a multiuser experience for up to ten users. We found that proximity-based interaction that encouraged dynamic movement positively affected social presence and physical/temporal workload. In bigger group settings, participants felt less challenged and less positive. Individuals had varying preferences for group size and interaction type. The findings of the study will advance our understanding of the design space for handheld-based MR in terms of group sizes and interaction schemes. To make our contributions explicit, we conclude our paper with design implications that can inform user experience design in handheld-based mixed reality contexts.
Understanding Online Parental Help-Seeking and Help-Giving in Early Childhood: The Design Challenges of Supporting Complex Parenting Questions
Authors: Ibrahim Seray , Ang Jazz Rui Xia , Petsolari Melina , Michelson Rebecca , Dong Yuzhen , Theofanopoulou Nikki , Van Kleek Max , Davis Katie , Slovák Petr
Published: April 2024

Early parenting is one of the strongest predictors of child well-being. Online social communities have shown promise in supporting parents across a range of contexts. However, we only have a limited understanding of how posters and commenters interact within a forum, or how well commenter responses can support complex parenting questions, such as attempts to change a child's behaviour or to apply new parenting approaches. We start addressing this gap by combining an empirical analysis of 1 year of parent posts from an exemplar online forum (Mumsnet) with literature on parenting interventions from psychology. In particular, we examine the types of question parents of 2-5 year olds seek help for around their children's behaviour, and the challenges with the support that they do (or do not) receive from the Mumsnet community. Combining empirical and theory-driven insights, we outline an 'information-to-application' gap that conceptually underpins the difficulties observed, and suggest plausible research directions that could address such design problems.
Dialoging Resonance in Human-Chatbot Conversation: How Users Perceive and Reciprocate Recommendation Chatbot's Self-Disclosure Strategy
Authors: Liang Kai-Hui , Shi Weiyan , Oh Yoo Jung , Wang Hao-Chuan , Zhang Jingwen , Yu Zhou
Published: April 2024

Using chatbots to make recommendations is increasingly popular. The design of recommendation chatbots has mainly been taking an information-centric approach by focusing on the recommended content per se. Limited attention is on how social connection and relational strategies, such as self-disclosure from a chatbot, may influence users' perception and acceptance of the recommendation. In this work, we designed, implemented, and evaluated a social chatbot capable of performing three different levels of self-disclosure: factual information (low), cognitive opinions (medium), and emotions (high). In the evaluation, we recruited 372 participants to converse with the chatbot on two topics: movies and COVID-19 experiences. In each topic, the chatbot conducted small talks and made relevant recommendations to the topic. Participants were randomly assigned to four experimental conditions where the chatbot used factual, cognitive, emotional, and adaptive strategies to perform self-disclosures. By training a text classifier to identify users' level of self-disclosure in real-time, the adaptive chatbot can dynamically match its self-disclosure language to the level of disclosure exhibited by the users. Our results show that users reciprocate with higher-level self-disclosure when a recommendation chatbot displays emotions throughout the conversation. The utilization of emotional disclosure by the chatbot resulted in enhanced enjoyment during interactions and a more favorable perception of the bot. This, in turn, led to greater effectiveness in making recommendations, including a higher likelihood of accepting the recommendation. We discuss the understandings obtained and implications to future design.
Field Trial of a Tablet-based AR System for Intergenerational Connections through Remote Reading
Authors: Yuan Ye , Genatempo Peter , Jin Qiao , Yarosh Svetlana
Published: April 2024

Prior work has explored various technology designs to support intergenerational communications and connections through remote activities such as reading or play. However, few works have explored these technologies outside the family settings. In this work, we aimed to understand how technology can support social connectedness through remote activities, by investigating the use of a tablet-based AR system among older adult volunteers and students for remote reading. We developed the system based on insights from previous research, deployed the system in the field, and observed the use of the system over six months. With the data collected from the field, we present a rich description on the use of the system and the practices that emerged around its usage in a real-world setting. Our findings highlight the importance of supporting an engaging reading experience and context understanding for social connections with the technology design. We provide insights into how such technology can support intergenerational communication and foster social connectedness.
"We Have No Idea How Models will Behave in Production until Production": How Engineers Operationalize Machine Learning
Authors: Shankar Shreya , Garcia Rolando , Hellerstein Joseph M. , Parameswaran Aditya G.
Published: April 2024

Organizations rely on machine learning engineers (MLEs) to deploy models and maintain ML pipelines in production. Due to models' extensive reliance on fresh data, the operationalization of machine learning, or MLOps, requires MLEs to have proficiency in data science and engineering. When considered holistically, the job seems staggering---how do MLEs do MLOps, and what are their unaddressed challenges? To address these questions, we conducted semi-structured ethnographic interviews with 18 MLEs working on various applications, including chatbots, autonomous vehicles, and finance. We find that MLEs engage in a workflow of (i) data preparation, (ii) experimentation, (iii) evaluation throughout a multi-staged deployment, and (iv) continual monitoring and response. Throughout this workflow, MLEs collaborate extensively with data scientists, product stakeholders, and one another, supplementing routine verbal exchanges with communication tools ranging from Slack to organization-wide ticketing and reporting systems. We introduce the 3Vs of MLOps: velocity, visibility, and versioning --- three virtues of successful ML deployments that MLEs learn to balance and grow as they mature. Finally, we discuss design implications and opportunities for future work.
Tinker, Tailor, Configure, Customize: The Articulation Work of Contextualizing an AI Fairness Checklist
Authors: Madaio Michael A. , Chen Jingya , Wallach Hanna , Wortman Vaughan Jennifer
Published: April 2024

Many responsible AI resources, such as toolkits, playbooks, and checklists, have been developed to support AI practitioners in identifying, measuring, and mitigating potential fairness-related harms. These resources are often designed to be general purpose in order to be applicable to a variety of use cases, domains, and deployment contexts. However, this can lead to decontextualization, where such resources lack the level of relevance or specificity needed to use them. To understand how AI practitioners might contextualize one such resource, an AI fairness checklist, for their particular use cases, domains, and deployment contexts, we conducted a retrospective contextual inquiry with 13 AI practitioners from seven organizations. We identify how contextualizing this checklist introduces new forms of work for AI practitioners and other stakeholders, as well as opening up new sites for negotiation and contestation of values in AI. We also identify how the contextualization process may help AI practitioners develop a shared language around AI fairness, and we identify tensions related to ownership over this process that suggest larger issues of accountability in responsible AI work.
Does More Advice Help? The Effects of Second Opinions in AI-Assisted Decision Making
Authors: Lu Zhuoran , Wang Dakuo , Yin Ming
Published: April 2024

AI assistance in decision-making has become popular, yet people's inappropriate reliance on AI often leads to unsatisfactory human-AI collaboration performance. In this paper, through three pre-registered, randomized human subject experiments, we explore whether and how the provision of second opinions may affect decision-makers' behavior and performance in AI-assisted decision-making. We find that if both the AI model's decision recommendation and a second opinion are always presented together, decision-makers reduce their over-reliance on AI while increase their under-reliance on AI, regardless whether the second opinion is generated by a peer or another AI model. However, if decision-makers have the control to decide when to solicit a peer's second opinion, we find that their active solicitations of second opinions have the potential to mitigate over-reliance on AI without inducing increased under-reliance in some cases. We conclude by discussing the implications of our findings for promoting effective human-AI collaborations in decision-making.
Networks and Influencers in Online Propaganda Events: A Comparative Study of Three Cases in India
Authors: Sen Anirban , De Soham , Pal Joyojeet
Published: April 2024

The structure and mechanics of organized outreach around certain issues, such as in propaganda networks, is constantly evolving on social media. We collect tweets on two propaganda events and one non-propaganda event with varying degrees of organized messaging. We then perform a comparative analysis of the user and network characteristics of social media networks around these events and find clearly distinguishable traits across events. We find that influential entities like prominent politicians, digital influencers, and mainstream media prefer to engage more with social media events with lesser degree of propaganda while avoiding events with high degree of propaganda, which are mostly sustained by lesser known but dedicated micro-influencers. We also find that network communities of events with high degree of propaganda are significantly centralized with respect to the influence exercised by their leaders. The methods and findings of this study can pave the way for modeling and early detection of other propaganda events, using their user and community characteristics.
Formalizing Multimedia Recommendation through Multimodal Deep Learning
Authors: Malitesta Daniele , Cornacchia Giandomenico , Pomo Claudio , Merra Felice Antonio , Di Noia Tommaso , Di Sciascio Eugenio
Published: April 2024

Recommender systems (RSs) provide customers with a personalized navigation experience within the vast catalogs of products and services offered on popular online platforms. Despite the substantial success of traditional RSs, recommendation remains a highly challenging task, especially in specific scenarios and domains. For example, human affinity for items described through multimedia content (e.g., images, audio, and text), such as fashion products, movies, and music, is multi-faceted and primarily driven by their diverse characteristics. Therefore, by leveraging all available signals in such scenarios, multimodality enables us to tap into richer information sources and construct more refined user/item profiles for recommendations. Despite the growing number of multimodal techniques proposed for multimedia recommendation, the existing literature lacks a shared and universal schema for modeling and solving the recommendation problem through the lens of multimodality. Given the recent advances in multimodal deep learning for other tasks and scenarios where precise theoretical and applicative procedures exist, we also consider it imperative to formalize a general multimodal schema for multimedia recommendation. In this work, we first provide a comprehensive literature review of multimodal approaches for multimedia recommendation from the last eight years. Second, we outline the theoretical foundations of a multimodal pipeline for multimedia recommendation by identifying and formally organizing recurring solutions/patterns; at the same time, we demonstrate its rationale by conceptually applying it to selected state-of-the-art approaches in multimedia recommendation. Third, we conduct a benchmarking analysis of recent algorithms for multimedia recommendation within Elliot, a rigorous framework for evaluating recommender systems, where we re-implement such multimedia recommendation approaches. Finally, we highlight the significant unresolved challenges in multimodal deep learning for multimedia recommendation and suggest possible avenues for addressing them. The primary aim of this work is to provide guidelines for designing and implementing the next generation of multimodal approaches in multimedia recommendation.
Assessing the Efficacy of Graphene, Graphene Oxide, and Graphene Oxide Encrusted with Gold Nanoparticles for Sulfur Removal from Crude Oil: An Innovative Experimental Investigation
Authors: Özkan Abdullah , Gördük Eyyüp
Published: April 2024

Crude oil, consisting of hydrocarbons, is the leading global energy source. Sulfur is the most abundant element after carbon and hydrogen in the structure of crude oil. Sulfur and sulfur compounds in the structure of petroleum are dangerous for both the environment and human health due to the SOx gases they produce after combustion. Removing sulfur from oil is a costly and difficult process. Therefore, the sulfur content of crude oil directly affects the price of oil. This study investigated the adsorptive desulfurization performance of graphene, graphene oxide, and graphene oxide functionalized with gold nanoparticles. The synthesized adsorbents were characterized by scanning electron microscopy, transmission electron microscopy, energy-dispersive X-ray analysis, reflection-absorption infrared spectroscopy, and X-ray photoelectron spectroscopy, and then 0.02 to 0.1 g adsorbents were taken separately and placed in a flask that included 50 ml of crude oil. Each flask was stirred at 400 rpm under ambient temperature for 1 h. After the reaction, the adsorbent was separated from the mixture with the help of a centrifuge, and the residual sulfur amount was checked. It was determined that the sulfur removal performance after 1 h contact time was between 2.09%–5.48% for Graphene, 1.91%–4.06% for GO, and 0.575%–6.471% for AuNPs/GO.
Mitochondria‐Associated Gene SLC25A32 as a Novel Prognostic and Immunotherapy Biomarker: From Pan‐Cancer Multiomics Analysis to Breast Cancer Validation
Authors: Zuo Shiqi , He Siyuan , Zhu Zhiqin , Zhang Yingying , Hou Yanjie , Wu Ziqing , Tang Yao
Published: April 2024

Background. Mutations in SLC25A32 in humans cause late‐onset exercise intolerance, which is associated with various neurological and metabolic diseases. However, its specific mechanism of action in tumour development is poorly understood owing to the lack of multiomics integrated analysis of SLC25A32 in pan‐cancer. Methods. We used various analytical tools to comprehensively investigate the transcription, protein level, and promoter methylation of SLC25A32. Furthermore, the GSCA and cBioPortal databases were used to evaluate the inheritance impact and epigenetic alterations of SLC25A32 in pan‐cancer. SLC25A32 expression and the prognostic significance of copy number alterations in multiple cancers were compared using the UCSCXenaShiny and GEPIA2.0 platforms, and its specific function in breast cancer was experimentally verified. Results. SLC25A32 is abnormally expressed at the transcriptional and protein levels in most cancer types, with aberrant DNA promoter methylation and significant gene amplification in most tumours. SLC25A32 is significantly associated with the survival prognosis of some cancers, immune infiltrating cells, tumour stemness, and immune‐related markers. SLC25A32 knockdown decreased breast tumour cell proliferation, invasion, and metastasis. Conclusions. This study aimed to reveal SLC25A32 as a novel prognostic biomarker for pan‐cancer prediction and immunotherapy efficacy and specifically describes its underlying mechanism of action in breast cancer. SLC25A32 is widely differentially expressed in pan‐cancer with prognostic significance and is correlated with immune infiltration. Additionally, it can affect breast cancer occurrence and development.
Large Bowel Internal Hernia Secondary to Reimplanted Ureter
Authors: Howk Amy A. , Hayden Anna , Griepentrog John E.
Published: April 2024

Internal hernias are difficult to diagnose clinically, and normal cross‐sectional imaging has been documented in many patients. Transmesenteric hernias from congenital defects or prior abdominal surgery are most common. A 46‐year‐old previously healthy female presented to the emergency department with acute onset nausea and vomiting eight years after a right ureteral transection during a laparoscopic hysterectomy, with a delayed ureterolysis and reimplantation into the bladder. Rectal contrast CT scan demonstrated a partial large bowel obstruction that was unclear if it was due to an underlying mass, stricture, or internal herniation. The patient was taken for exploratory laparotomy which demonstrated redundant transverse colon herniated under the mobile right ureter; an extended right hemicolectomy was performed. This report describes alteration of retroperitoneal anatomy creating a potential space for colonic herniation and emphasizes that clinical suspicion must remain high for patients presenting with obstructive or partially obstructive symptoms.