34 citations · 94 across the 11 of their papers we have counts for
11 papers · 1 filter
Lilac: A Modal Separation Logic for Conditional Probability
John M. Li, Amal Ahmed, Steven Holtzen
We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutabl…
Oxide: The Essence of Rust
Aaron Weiss, Olek Gierczak, Daniel Patterson +1
Rust claims to advance industrial programming by bridging the gap between low-level systems programming and high-level application programming. At the heart of the argument that th…
Gradual Type Theory (Extended Version)
Max S. New, Daniel R. Licata, Amal Ahmed
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type…
Typed Closure Conversion for the Calculus of Constructions
William J. Bowman, Amal Ahmed
Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these…
Graduality from Embedding-projection Pairs (Extended Version)
Max S. New, Amal Ahmed
Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about these mixed programs i…
Rust Distilled: An Expressive Tower of Languages
Aaron Weiss, Daniel Patterson, Amal Ahmed
Rust represents a major advancement in production programming languages because of its success in bridging the gap between high-level application programming and low-level systems…
Correctness of Speculative Optimizations with Dynamic Deoptimization
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee +3
High-performance dynamic language implementations make heavy use of speculative optimizations to achieve speeds close to statically compiled languages. These optimizations are typi…
Linking Types for Multi-Language Software: Have Your Cake and Eat It Too
Daniel Patterson, Amal Ahmed
Software developers compose systems from components written in many different languages. A business-logic component may be written in Java or OCaml, a resource-intensive component…
FunTAL: Reasonably Mixing a Functional Language with Assembly
Daniel Patterson, Jamie Perconti, Christos Dimoulas +1
We present FunTAL, the first multi-language system to formalize safe interoperability between a high-level functional language and low-level assembly code while supporting composit…
FabULous Interoperability for ML and a Linear Language
Gabriel Scherer, Max New, Nick Rioux +1
Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate…
Database Queries that Explain their Work
James Cheney, Amal Ahmed, Umut A. Acar
Provenance for database queries or scientific workflows is often motivated as providing explanation, increasing understanding of the underlying data sources and processes used to c…