These abstracts are for talks at this event.
NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source.
A Spectrum of Type Soundness and Performance
Ben Greenman (Northeastern University)
(preview of an ICFP 2018 talk) Most gradual typing systems in the literature come with a "type soundness" guarantee. But despite the common name, different systems' notions of type soundness are often fundamentally different. The differences affect performance and the predictive power of static types. This talk explains: (1) why type soundness matters, (2) why it is difficult/undesirable for a gradually-typed language to be type-sound, and (3) three alternative "type soundnesses" from the literature.
Probabilistic Reactive Programming
Louis Mandel (IBM)
The idea of Probabilistic Programming is to use the expressiveness of programming languages to build probabilistic models. To implement this idea, a common approach is to take a general purpose language and extend it with (1) a function that allows to sample a value from a distribution, (2) a function that allows to condition values of variables in a program via observations, and (3) an inference procedure that build a distribution for a program using the two previous constructs. Following this approach, we propose to extends a reactive programming language with probabilistic constructs. This new language enables the modeling of probabilistic reactive systems, that is, probabilistic models in constant interaction with their environment. Examples of such systems include time-series prediction, agent-based systems, or infrastructure self-tuning. To demonstrate this approach, we started from ReactiveML, a reactive extension of OCaml that supports parallel composition of processes, communication through signals, preemption, and suspension. We extend the language with classic probabilistic constructs (sample, factor à la WebPPL) and propose an inference scheme for reactive processes, that are, non-terminating functions.
Opportunities to Simplify Computer Systems via Formal Methods
Adam Chlipala (MIT)
It's an exciting time for machine-checked proofs that computer systems do what they are supposed to do. With this technology getting more and more practical, it's worth asking: how could we simplify and improve the design of computer systems, knowing that mechanized proof is an available ingredient? Are the traditional APIs connecting layers the right ones? I propose to share my answers to those questions, mostly considering functionality usually associated with computer architecture, operating systems, compilers, and databases. Though I would expect to spend a little time on systems that have already been built, my main focus would be on a plan for a simple end-to-end verified prototype system, with rationale for why it should work well.
Ergo: Designing a Strongly Typed DSL for Executable Legal Contracts
Kartik Chandra (Stanford University/Clause, Inc.)
Programming Music by Example: Synthesizing Digital Signal
Mark Santolucito (Yale University)
Programming-by-example allows users to create programs without coding by simply specifying input and output pairs. We introduce the problem of digital signal processing programming by example (DSP-PBE), where users specify input and output audio wave files, and a tool automatically synthesizes a program that transforms the input to the output. This program can then be applied to new wave files, giving users a new way to interact with music and program code. We formally define the problem of DSP-PBE, and provide a first implementation of a solution that can handle synthesis over commutative filters. In digital signal processing for audio, two wave files may have very different values, but sound very similar. Thus, DSP-PBE faces the unique challenge in the space of program synthesis as the measure of correctness is not directly derived from the output of the program. Instead of searching for a program that will produce the same values as the example, we must search for a program with the same audio profile as the examples. In this talk, we describe the combination of refinement type-based synthesis and gradient descent to explore the space of programs with respect to a measure of audio profile distance.
Anomaly detection in C API usage
Tiago Cogumbreiro (University of Massachusetts Boston)
This talk focuses on the problem of automatic ad-hoc specification of APIs at large. Our technique leverages existing code bases by inferring a probabilistic specification from how APIs are used. With a learned specification, our tool statically analysis source code for anomalous buggy API usage, which tends to be buggy. We introduce Salento 2.0, the new version of our Bayesian framework for learning probabilistic specifications, which introduces support for C, as well as novel anomaly metrics that support the characteristics of C APIs. We evaluate a learned specification from the glib API, discuss how anomaly metrics identify different kinds of anomalies, and discuss existing software defects automatically identified by Salento.
Our tool is open source and freely available at https://github.com/capergroup/salento.
Going Green: Compositional Non-termination without Fuel in Coq
Gregory Malecha (Kevix)
Gallina, the language of the Coq proof assist, is a language of total functions which, by Curry-Howard, double as proofs. While convenient for proving, the totality requirement makes it difficult to give denotational semantics of non-terminating languages into Gallina. A common approach is to use fuel but this can be problematic for programs that do I/O because the number of steps may depend on the input. In this work I show how to define a fixpoint combinator based on co-inductive types. The combinator guarantees productivity/guardedness which is a syntactic check in Coq that ensures soundness of co-inductive computations. On top of this combinator, we can give denotational semantics to linking mutually recursive programs. Current work is focused on reasoning about programs written in this style.
Run-Time Program-Specific Phase Prediction for Python Programs
Meng-Chieh Chiu (University of Massachusetts Amherst)
It is well-known that a program's execution can be partitioned into different phases. Because of their impact on micro-architectural components such as caches and branch predictors, phases are an important aspect of dynamic program behavior that is useful in analyzing performance and energy consumption. They are also relevant to detecting whether a program is executing as expected, which helps software engineers in program analysis and understanding. We develop here a method for run-time phase prediction for Python programs. After training on different runs of each program of interest, our method can predict the future phase k steps later, for k = 1, ..., at run time, for a new run of the same program but on different inputs, with good precision and recall (compared with a "ground truth" definition of phases) and with small run-time overhead (average less than 1%).
Kleene algebra modulo theories
Michael Greenberg (Pomona College)
Are you working on something that can be modeled in terms of simple While programs over some decidable domain? Kleene algebra modulo theories (KMT) is a pay-as-you-go approach for sound, complete, and decidable models of simple programs. The KMT metatheory corresponds directly to an automata-theoretic implementation strategy: for just a few lines of code describing your theory's syntax and decision procedure, we can decide equivalences between While programs that use your theory.
|Last modified Friday, August 24th, 2018 4:54:20pm|