48 citations · 129 across the 13 of their papers we have counts for
15 papers · 1 filter
Absynthe: Abstract Interpretation-Guided Synthesis
Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
Synthesis tools have seen significant success in recent times. However, past approaches often require a complete and accurate embedding of the source language in the logic of the u…
A Formal Model of Checked C
Liyi Li, Yiyun Liu, Deena L. Postol +3
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, potent…
RbSyn: Type- and Effect-Guided Program Synthesis
Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
In recent years, researchers have explored component-based synthesis, which aims to automatically construct programs that operate by composing calls to existing APIs. However, prio…
Type-Level Computations for Ruby Libraries
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou +2
Many researchers have explored ways to bring static typing to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often aris…
Constructive Galois Connections
David Darais, David Van Horn
Galois connections are a foundational tool for structuring abstraction in semantics and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of…
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell)
Niki Vazou, Joachim Breitner, Will Kunkel +2
Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manua…