Mid Atlantic Programming Languages Seminar

University of Maryland, College Park

April 5^th, 2013

The 2013 Mid Atlantic Programming Languages Seminar (MALPS) will be held at the University of Maryland, College Park. The meeting will be on April 5th, and at the University of Maryland campus.

Lunch for MAPLS is supported by a gift from Northrop-Grumman.

Directions

Directions to the department and information about parking can be found here. The meeting will be in the CSIC building (adjacent to AV Williams), in room 3118 (the third floor). Floorplans for CSIC are here. A campus map is linked here. CSIC is quadrant E4, building 406. The visitor lot is in the middle of quadrant E4 (there's a [P] in the middle of it).

Agenda

Abstracts

Design-Driven Software Development: A Programming Language-Inspired Approach

Charles Consel — Inria / University of Bordeaux

Raising the level of abstraction beyond programming is a very active research topic involving a range of areas, including software engineering, programming languages and formal verification. The challenge is to allow design dimensions of a software system, both functional and non-functional, to be expressed in a high-level way, instead of being encoded with a programming language. Such design dimensions can then be leveraged to verify conformance properties and to generate programming support.

Our research on this topic is to take up this challenge with an approach inspired by programming languages, introducing a full-fledged language for designing software systems and processing design descriptions both for verification and code generation purposes. Our approach is also inspired by domain-specific languages in that it defines a conceptual framework to guide software development. Lastly, to make our approach practical to software developers, we introduce a methodology and a suite of tools covering the development life-cycle.

This talk gives an overview of our approach and presents our main research results, illustrated by concrete examples.

A Core Calculus for Mixed-mode Secure Multi-party Computations

Matthew Hammer — UMD

In a Secure Multi-party Computation (SMC), mutually-distrusting parties cooperate to compute over their private data; parties only learn information that is explicitly revealed as per the agreed protocol. Standard implementations of SMC, e.g., using garbled circuits, can be very slow, so researchers have begun to explore what we call mixed-mode secure computations that combine standard SMCs with local computations, resulting in orders of magnitude speedups. Ultimately, we would like to produce a compiler that takes "ordinary code" and compiles it into mixed-mode SMC. As a step in this direction, this paper presents a core calculus that aims to capture the essence of mixed-mode SMCs, and their compilation to realizable protocols. Our approach builds on Levy's call-by-push-value calculus, and permits one to specify where a computation occurs, which computations are done locally versus securely, and also which state is carried over from one secure computation to another. We show that a well-typed program in core calculus is sound (it does not get stuck), is secure (parties learn only what the protocol prescribes), compiles properly to a target protocol, and that the operational semantics of the source program corresponds to the operational semantics of the target protocol. We show that our framework is elegant, expressive, and practical by showing how it elucidates several recently published optimized protocols, and that it naturally supports reasoning about even more general compositions of such protocols.

Big Bang

Scott Smith — JHU

This talk describes a new programming language we are designing and building, Big Bang. Big Bang uses highly flexible inferred types to achieve a combination of flexible coding style, is designed for fast runtimes, and ease of debugging. The design builds on many ideas from the PL literature: type inference, subtype constraints, typed record concatenation, first-class cases, type-indexed records, and adaptive polymorphism, to achieve a sum greater than its parts. We will cover examples which show the flexibility: even without using explicit object syntax, Big Bang type-checks object extension examples more flexibly than any existing language.

Polymonads

Michael Hicks — UMD

From their semantic origins to their use in structuring effectful computations, monads are now also used as a programming pattern to structure code in a number of important scenarios, including for program verification, for information flow tracking, to compute complexity bounds, and for defining precise type-and-effect analyses. However, whilst these examples are inspired by monads they are not strictly speaking monadic but rather something more general. The first contribution of this paper is the definition of a new categorical structure, the polymonad, which explains these not-quite-monadic constructions, and subsumes well-known concepts including monads, layered monads, and systems of monads and monad morphisms, among others.

We show how to interpret polymonads in the setting of System Fω. While this interpretaion enables several useful programming idioms, programming directly with polymonads in Fω is far from convenient. Addressing this concern, the second contribution of this paper is core ML-like programming language, λPM, with a polymorphic type inference algorithm that infers a principal polymonadic type for a program and elaborates it to Fω in a coherent way---all unambiguous typing derivations produce elaborated programs with the same semantics. The resulting programming style in λPM is powerful and lightweight, as we demonstrate through a series of examples.

Abstracting Definitional Interpreters

David Van Horn — Northeastern University

Definitional interpreters written in monadic style can express a wide variety of interpreters for languages with effects. In this talk, we show that such interpreters, under a slight reworking, can also express a diverse set of abstract interpretations from flow analysis to symbolic execution.

We give a rational reconstruction of a definitional abstract interpreter for a higher-order language by constructing a series of units implementing monadic operations. We implement units realizing reachable state semantics, trace semantics, dead-code elimination, symbolic execution, and a finite store abstraction. The denouement of our story is a sound and computable abstract interpreter that arises from the composition of simple, independent components. Remarkably, this interpreter implements a form of pushdown control flow analysis (PDCFA) in which calls and returns are always properly matched in the abstract semantics. True to the definitional style of Reynolds, the evaluator involves no explicit mechanics to achieve this property; it is simply inherited from the defining language.

HyperLTL

Masoud Koleini — George Washington University

In this work, we introduce HyperLTL, a logic based on LTL that is capable of expressing security properties, such as noninterference, generalized noninterference, and observational determinism. LTL cannot directly express such properties, but HyperLTL can, because it extends LTL with explicit quantification over paths and with purge operators.

We also present ongoing work on a model-checking algorithm to verify HyperLTL formulas. The current algorithm suffices to verify many information-flow properties, but is not yet capable of handling one particular kind of formula (conjunction of purged sub-formulas).

HyperLTL is designed for verification of hyperproperties, a formalism that is general enough to express all known security properties. Hyperproperties currently lack a general verification methodology, but HyperLTL is a step toward one. Joint work with Michael Clarkson.

A Logical Revolution

Moshe Vardi — Rice

(This talk is in room 1110 of the Kim Engineering Building. We will be walking over after the last MAPLS session.) Starting from the mid 1970s, there has been a quiet revolution in logic in computer science, and problems that are theoretically undecidable or intractable were shown to be quite feasible in practice. This talk describes the rise, fall, and rise of logic in computer science, describing several modern applications of logic to computing, include databases, hardware design, and software engineering.

Web Accessibility