49 citations · 105 across the 20 of their papers we have counts for
24 papers
Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types
Siyuan He, Songlin Jia, Tiark Rompf
Subtyping provides polymorphism at a low cost: a concise type such as Int Top covers every function that accepts an integer, whatever it returns, whereas the parametric alter…
Capture Now, Consume Later: Reachability Types with Flow-Sensitive Effects for Higher-Order Ownership Transfer
Haotian Deng, Siyuan He, Songlin Jia +2
Higher-order impure programs routinely transfer or consume a resource through a closure: when one access path consumes the resource, it must be disabled through all remaining alias…
Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness
Yuyan Bao, Tiark Rompf
Programming benefits from a clear separation between pure, mathematical computation and impure, effectful interaction with the world. Existing approaches to enforce this separation…
Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He +3
Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. For example, scope-based construct…
When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
Siyuan He, Songlin Jia, Yuyan Bao +1
Static resource management in languages remains challenging due to tensions among control, expressiveness, and flexibility. Region-based systems [Grossman et al . 2002; Tofte et al…
Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
Haotian Deng, Siyuan He, Songlin Jia +2
Local reasoning about programs that combine aliasing and mutable state is a longstanding challenge. Existing approaches -- ownership systems, linear and affine types, uniqueness ty…
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He +2
Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popularized lifetime-based ownership tracking in systems programming, but its "…
Architecting Intermediate Layers for Efficient Composition of Data Management and Machine Learning Systems
Supun Abeysinghe, Fei Wang, Gregory Essertel +1
Modern data analytics workloads combine relational data processing with machine learning (ML). Most DBMS handle these workloads by offloading these ML operations to external specia…
Graph IRs for Impure Higher-Order Languages (Technical Report)
Oliver Bračevac, Guannan Wei, Songlin Jia +4
This is a companion report for the OOPSLA 2023 paper of the same title, presenting a detailed end-to-end account of the graph IR, at a level of detail beyond a r…
Modeling Reachability Types with Logical Relations
Yuyan Bao, Songlin Jia, Guannan Wei +2
Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages, with a focus on higher-order functions, parametric types,…
OCTAL: Graph Representation Learning for LTL Model Checking
Prasita Mukherjee, Haoteng Yin
Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, suffer from the sta…
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Guannan Wei, Oliver Bračevac, Songlin Jia +2
Reachability types are a recent proposal that has shown promise in scaling to higher-order but monomorphic settings, tracking aliasing and separation on top of a substrate inspired…
OCTAL: Graph Representation Learning for LTL Model Checking
Prasita Mukherjee, Haoteng Yin, Susheel Suresh +1
Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from t…
A GNN Based Approach to LTL Model Checking
Prasita Mukherjee, Tiark Rompf
Model Checking is widely applied in verifying complicated and especially concurrent systems. Despite of its popularity, model checking suffers from the state space explosion proble…
HACCLE: Metaprogramming for Secure Multi-Party Computation -- Extended Version
Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik +17
Cryptographic techniques have the potential to enable distrusting parties to collaborate in fundamentally new ways, but their practical implementation poses numerous challenges. An…
Resilient Cyberphysical Systems and their Application Drivers: A Technology Roadmap
Somali Chaterji, Parinaz Naghizadeh, Muhammad Ashraful Alam +14
Cyberphysical systems (CPS) are ubiquitous in our personal and professional lives, and they promise to dramatically improve micro-communities (e.g., urban farms, hospitals), macro-…
Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers
Zhanfu Yang, Fei Wang, Ziliang Chen +2
In this paper, we investigate the feasibility of learning GNN (Graph Neural Network) based solvers and GNN-based heuristics for specified QBF (Quantified Boolean Formula) problems.…
AutoGraph: Imperative-style Coding with Graph-based Performance
Dan Moldovan, James M Decker, Fei Wang +6
There is a perceived trade-off between machine learning code that is easy to write, and machine learning code that is scalable or fast to execute. In machine learning, imperative s…
Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
Fei Wang, Daniel Zheng, James Decker +3
Deep learning has seen tremendous success over the past decade in computer vision, machine translation, and gameplay. This success rests in crucial ways on gradient-descent optimiz…
From Gameplay to Symbolic Reasoning: Learning SAT Solver Heuristics in the Style of Alpha(Go) Zero
Fei Wang, Tiark Rompf
Despite the recent successes of deep neural networks in various fields such as image and speech recognition, natural language processing, and reinforcement learning, we still face…
Flare: Native Compilation for Heterogeneous Workloads in Apache Spark
Grégory M. Essertel, Ruby Y. Tahboub, James M. Decker +3
The need for modern data analytics to combine relational, procedural, and map-reduce-style functional processing is widely recognized. State-of-the-art systems like Spark have adde…
Building Efficient Query Engines in a High-Level Language
Amir Shaikhha, Yannis Klonatos, Christoph Koch
Abstraction without regret refers to the vision of using high-level programming languages for systems development without experiencing a negative impact on performance. A database…
From F to DOT: Type Soundness Proofs with Definitional Interpreters
Tiark Rompf, Nada Amin
Scala's type system unifies ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new foundation for Sc…
Building-Blocks for Performance Oriented DSLs
Tiark Rompf, Arvind K. Sujeeth, HyoukJoong Lee +4
Domain-specific languages raise the level of abstraction in software development. While it is evident that programmers can more easily reason about very high-level programs, the sa…