17 citations · 38 across the 6 of their papers we have counts for
11 papers
Lava: Foundations for Liquid Haskell via Translation to Rocq
Colin Rothgang, Loïc Peyrot, Yannick Forster +2
Liquid Haskell is an extension of the Glasgow Haskell compiler (GHC) that adds support for refinement types: types restricted by logical predicates. Specifications are automaticall…
MultiPL-E: A Scalable and Extensible Approach to Benchmarking Neural Code Generation
Federico Cassano, John Gouwar, Daniel Nguyen +10
Large language models have demonstrated the ability to generate both natural language and programming language text. Such models open up the possibility of multi-language code gene…
Solver-based Gradual Type Migration
Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg +1
Gradually typed languages allow programmers to mix statically and dynamically typed code, enabling them to incrementally reap the benefits of static typing as they add type annotat…
Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
Eric Campbell, Michael Greenberg
Temporal logics over finite traces are not the same as temporal logics over potentially infinite traces. Roşu first proved completeness for linear temporal logic on finite traces (…
How to Safely Use Extensionality in Liquid Haskell
Niki Vazou, Michael Greenberg
Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation, porting the proofs t…
Formulog: Datalog for SMT-Based Static Analysis (Extended Version)
Aaron Bembenek, Michael Greenberg, Stephen Chong
Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We prop…
Executable formal semantics for the POSIX shell
Michael Greenberg, Austin J. Blatt
The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert's control panel, a necessary tool for configuring, compiling, installing,…
Kleene Algebra Modulo Theories
Michael Greenberg, Ryan Beckett, Eric Campbell
Kleene algebras with tests (KATs) offer sound, complete, and decidable equational reasoning about regularly structured programs. Interest in KATs has increased greatly since NetKAT…
Space-Efficient Latent Contracts
Michael Greenberg
Standard higher-order contract monitoring breaks tail recursion and leads to space leaks that can change a program's asymptotic complexity; space-efficiency restores tail recursion…
SNAP: Stateful Network-Wide Abstractions for Packet Processing
Mina Tahmasbi Arashloo, Yaron Koral, Michael Greenberg +2
Early programming languages for software-defined networking (SDN) were built on top of the simple match-action paradigm offered by OpenFlow 1.0. However, emerging hardware and soft…
Space-Efficient Manifest Contracts
Michael Greenberg
The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program's asymptotic space complexity.…