11 citations · 15 across the 2 of their papers we have counts for
6 papers
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…
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…