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.)

We present Ergo, a new domain-specific language for writing executable
legal contracts. Ergo is designed to be accessible to programmers and
lawyers alike. Ergo programs are structured by assembling individual
executable clauses into a contract. The contract's logic is then
connected to its legal text through a templating mechanism.

In this presentation, we illustrate Ergo using examples taken from
real-life legal contracts. We also describe Ergo's design and compiler
infrastructure. From a PL perspective, Ergo incorporates ideas from
both functional and object-oriented languages. To ensure the safety of
contract execution, Ergo is strongly typed: every call to a contract
is guaranteed to terminate without a runtime error. The Ergo compiler
is written in Coq with the goal of providing formal semantics and
verifying parts of the compilation chain. The compiler currently emits
JavaScript to be executed on Node.js servers, with planned extensions
for executing contracts on the JVM and on distributed ledgers.

Ergo is under active development as part of the Accord Project, a
consortium of both technology companies and law firms that is
developing open-source software for legally enforceable smart
contracts.

Ergo language, Accord project. Authors: Jerome Simeon (Clause, Inc.), Joseph J. Bambara (UCNY), Kartik Chandra (Stanford University/Clause, Inc.), and Matt Roberts (Clause, Inc.).

Programming Music by Example: Synthesizing Digital Signal Processing Programs

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.

blog post, GitHub Coq development

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