NJPLS @ Stevens
Bissinger Room (4th floor of Howe) — Friday, May 6th, 2022
This run of NJPLS will be in-person only, with no accommodations for hybrid or remote participation. If there are, e.g., new variants or university policy changes, we will simply cancel the event.
Per Stevens policy, masks will be required.
If you're driving to Hoboken and need parking, download and print a parking permit before you come. Park in the Babbio garage and walk to Howe. Please register by Friday, April 29!
Please distribute and post our flyer, too!
Program
9:00am | – | 10:00am | Breakfast (catered) |
10:00am | – | 11:00am |
Xiaodong Jia (Penn State)
Konstantinos Kallas (UPenn)
Peter Thiemann (Uni. Freiburg)
|
11:00am | – | 12:00pm | Santosh Nagarakatte (Rutgers) |
12:00pm | – | 1:30pm | Lunch (catered) |
1:30pm | – | 2:30pm |
Sebastian Wolff (NYU)
Ryan Kavanagh (McGill)
Adam Chen (Stevens)
|
2:30pm | – | 3:00pm | Coffee break (catered) |
3:00pm | – | 4:00pm |
Sankha Narayan Guria (UMD)
Li–yao Xia (UPenn)
Nisarg Patel (NYU)
|
4:00pm | – | 4:15pm | Break |
4:15pm | – | 5:15pm |
Harrison Goldstein (UPenn)
Joshua Cohen (Princeton)
Jacob Prinz (UMD)
|
5:15pm | – | 5:30pm | Business Meeting |
5:30pm | – | Drinks and dinner out on the town |
Abstracts
A Verified Parser Generator for Visibly Pushdown Grammars
PaSh: Light-touch Parallelization for Shell Scripts
Polymorphic Imperative Session Types
We show that higher-order polymorphism and existential types are key to lift the restrictions imposed by previous work. On this bases, we define PolyVGR, the system of polymorphic imperative session types and establish its basic metatheory, type preservation and progress.
KEYNOTE: A Case for Correctly Rounded Elementary Functions
In contrast, we make a case for approximating the correctly rounded result of an elementary function rather than the real value of an elementary function in the RLIBM project. Once we approximate the correctly rounded result, there is an interval of real values around the correctly rounded result such that producing a real value in this interval rounds to the correct result. This interval is the freedom that the polynomial approximation has for an input, which is larger than the ones with the mini-max approach. Using these intervals, we structure the problem of generating polynomial approximations that produce correctly rounded results for all inputs as a linear programming problem. The results from the RLIBM project makes a strong case for mandating correctly rounded results with any representation that has fewer than or equal to 32-bits.
Bio: Santosh Nagarakatte is an Associate Professor and Undergraduate Program Director of Computer Science at Rutgers University. He obtained his PhD from the University of Pennsylvania in 2012. His research interests are in Hardware-Software Interfaces spanning Programming Languages, Compilers, Software Engineering, and Computer Architecture. His papers have been selected as IEEE MICRO Top Picks papers of computer architecture conferences in 2010 and 2013. He received the NSF CAREER Award in 2015, ACM SIGPLAN PLDI 2015 Distinguished Paper Award, and ACM SIGSOFT ICSE 2016 Distinguished Paper Award for his research on LLVM compiler verification. His papers have also been selected as the 2016 SIGPLAN Research Highlights Paper and 2018 Communication of the ACM Research Highlights Paper. His PhD student David Menendezβs dissertation was awarded the John C Reynolds ACM SIGPLAN Outstanding Dissertation Award in 2018. His papers on correctly rounded elementary functions have been recognized with the ACM SIGPLAN PLDI 2021 Distinguished Paper Award and the ACM SIGPLAN POPL 2022 Distinguished Paper Award.
A Concurrent Program Logic with a Future and History
Channel-Dependent Session Types
In this talk, we present preliminary results on channel-dependent session types (CDSTs). CDSTs use a restricted form of concurrent type-level computation to capture a richer class of communication protocols than allowed by traditional binary session types. In particular, CDSTs can observe communications on other channels used by a process and then use these observations to restrict the communications permitted on session-typed channels. We show how to use CDSTs to specify communication protocols with various desirable causal and temporal properties.
Veracity: Declarative Multicore Programming with Commutativity
In this talk, we will discuss our proposed paradigm in which programmers write programs in a familiar, sequential manner, with the added ability to explicitly express the conditions under which code fragments commute. Putting such commutativity conditions into source code offers a new entry point to exploit the known connection between commutativity and parallelism. We give sequential and concurrent semantics for commute statements, as well as a correctness condition called scoped serializability and discuss how it can be enforced when combined with commutativity conditions.
We will next describe a technique for automatically synthesizing commute conditions directly from source code. We will demonstrate our new language Veracity, commutativity synthesis tools, and runtime implemented in Multicore OCaml on top of Servois and libcuckoo, a state-of-the-art concurrent hashtable. We will show how to verify and synthesize commute conditions for a variety of programs and the speedup that can be obtained from exploiting commutativity.
Absynthe: From Abstract Interpretation to Program Synthesis
The lazy demands and the clairvoyant costs
Verifying Concurrent Multicopy Search Structures
Reflecting on Random Generation
In this talk, I'll present reflective generators, a modified DSL for random generation that builds on ideas from bidirectional programming to improve workflows throughout the testing process. Reflective generators can do more than just sample input values: they can validate their own correctness, adapt their distributions based on user-specified examples, and even mutate test inputs while maintaining invariants. These new capabilities come at a relatively low cost and unlock state-of-the-art testing strategies that normally require entirely separate testing infrastructure.
Verified Erasure Correction in Coq with MathComp and VST
In this talk, we present a formal, machine-checked proof of a C implementation of erasure correction based on Reed-Solomon coding. The C code has been actively used in network defenses for over 25 years, but the correctness of certain optimizations it uses was previously unknown. To prove this code correct, we had to both reason about the algorithm, which is based on finite fields, linear algebra, and polynomials, as well as prove that the C program correctly implements this algorithm. These proofs are both highly nontrivial but are quite different; we use Coq's Mathematical Components library for the former and the Verified Software Toolchain for the latter (after correcting a latent bug). This is the first end-to-end, formal proof of a real-world erasure code, and the first time that MathComp and VST, two very different Coq libraries with conflicting types, tactics, and proof styles, were used together.
Deeper Shallow Embeddings
In this paper, we attempt to bridge the gap between the two, by presenting a general technique for extending a shallow embedding of a type theory with a deep embedding of its typing derivations. Such embeddings are almost as straightforward to implement as shallow ones, but come with capabilities traditionally associated with deep ones. We demonstrate these increased capabilities in a number of case studies; including a DSL that only holds affine terms, and a dependently typed core language with computational beta reduction that leverages function extensionality.
Talk proposals
Talk proposals were due on Wednesday, April 6th. There were twenty on-time proposals.
Contact info
You can join the NJPLS mailing list to stay up-to-date on future events. If you have questions about this run of NJPLS at Stevens, contact Michael Greenberg.