Programming Languages Retreat 2015

Date: August 17
Location: Highland Lodge
Organizers: Fabian Muehlboeck and Nate Foster
Previous Semesters: Archives


Highland Lodge Center

Every year, the Cornell Programming Language Discussion Group (PLDG) holds an off-site retreat. The objective of the retreat is to give students and faculty an opportunity to get feedback on their current work in a friendly setting. We will also have a sessions devoted to discussing broader research trends and challenges, tool demos, and a keynote by Tom Reps!


The retreat will be held at the Highland Lodge Center in Trumansburg.

Directions: Take 96 North to Trumansburg. You will pass the Rongovoian Embassy, a row of shops in Trumansburg Village, and the Post Office on left. Take the first LEFT after the Post Office onto Rte 227 and drive 2.6 miles to Indian Fort Rd. Turn left. Half mile and second mailbox on left. 5176 Indian Fort Rd. See blue Highland Lodge Center sign on left.


Time Topic Presenter  
9:30-10:30Automating Abstract InterpretationTom RepsDetails

Unfortunately, the problem of determining whether a program is correct is undecidable. Program-analysis and verification tools sidestep the tar-pit of undecidability by working on an abstraction of a program, which over-approximates the behavior of the original program. The theory underlying this approach is called abstract interpretation. Abstract interpretation provides a way to obtain information about the possible states that a program reaches during execution, but without actually running the program on specific inputs. Instead, it explores the program's behavior for all possible inputs, thereby accounting for all possible states that the program can reach. Operationally, one can think of abstract interpretation as running the program "in the aggregate". That is, rather than executing the program on ordinary states, the program is executed on abstract states, which are finite-sized descriptors that represent collections of states.

However, there is a glitch: abstract interpretation has a well-deserved reputation of being a kind of "black art", and consequently difficult to work with. This talk will describe a twenty-year quest address this issue by raising the level of automation in abstract interpretation. I will present several different approaches to creating correct-by-construction analyzers. Somewhat surprisingly, this research has recently allowed us to establish connections between our problem and several other areas of computer science, including machine learning, knowledge compilation, data integration, and constraint programming.

(Joint work with Aditya Thakur and a variety of students over several years.)

Speaker Bio

Note: these are excerpts from

Thomas W. Reps is the J. Barkley Rosser Professor & Rajiv and Ritu Batra Chair in the Computer Sciences Department of the University of Wisconsin, which he joined in 1985. Reps is the author or co-author of four books and more than one hundred seventy-five papers describing his research (see His work has concerned a wide variety of topics, including program slicing, dataflow analysis, pointer analysis, model checking, computer security, code instrumentation, language-based program-development environments, the use of program profiling in software testing, software renovation, incremental algorithms, and attribute grammars.

His collaboration with Professor Tim Teitelbaum at Cornell University from 1978 to 1985 led to the creation of two systems—the Cornell Program Synthesizer and the Synthesizer Generator—that explored how to build interactive programming tools that incorporate knowledge about the programming language being supported. The systems that they created were similar to modern program-development environments, such as Microsoft Visual Studio and Eclipse, but pre-dated them by more than two decades. Reps is President of GrammaTech, Inc., which he and Teitelbaum founded in 1988 to commercialize this work.

Professor Reps received his Ph.D. in Computer Science from Cornell University in 1982. His Ph.D. dissertation won the 1983 ACM Doctoral Dissertation Award.

Reps has also been the recipient of an NSF Presidential Young Investigator Award (1986), a Packard Fellowship (1988), a Humboldt Research Award (2000), and a Guggenheim Fellowship (2000). He is also an ACM Fellow (2005). In 2013, Reps was elected a foreign member of Academia Europaea.

10:30-11:00Coffee Break
11:00-11:20Secure Distributed Transactions With Information Flow RestrictionsIsaac SheffDetails

Atomic Transactions are a popular programming abstraction for distributed systems. However, when a system incorporates elements in different trust domains, the scheduling and commit procedures for transactions may themselves leak information. Two-phase commit, for example, can issue ""abort"" messages to everyone involved in a transaction, revealing that one participant is busy with some other transaction.

In our ongoing work, we explore the limits of distributed, secure transaction commits. We demonstrate that monotonically increasing security levels are sufficient to create a safe scheduling algorithm for single-threaded transactions, even in an open system (where not all possible transactions are known in advance), and provide examples of impossible-to-schedule transactions, with an eye toward deriving even more permissive, safe scheduling in some circumstances.

11:20-11:40Tool Demo: An Extensible IDE Framework for Polyglot LanguagesJed Liu
11:40-12:00Effect TokensAndrew K. HirschDetails

Effect tokens are a way of representing the ordering effects impose on a program graph. However, current techniques for deciding when to force ordering are naive. This talks describes our current project, which looks into the mathematical foundations of effect tokens, and when we can soundly not force sequencing in the face of effectful computations.

13:30-14:10PL Quizzo
14:10-14:30Making Subtyping more Intelligent via PreprocessingFabian MuehlboeckDetails

Advanced type-system features often interact with subtyping in ways that make it difficult to algorithmically prove certain intended subtyping relationships. In particular, introducing intersection and union types into an otherwise nominal object-oriented type system produces several hard cases for algorithmic subtyping, such as distributivity of intersections through unions. For this reason, existing languages that feature intersection and union types often do not support distributivity, among other features, even though distributivity is the easiest of the features that we are addressing.

We present a general strategy of preprocessing types to make subtyping more intelligent. We apply this strategy to distributivity, disjointness of types, and consolidating cases of sum types. Moreover, we extend this strategy to work in the presence of variant generics, addressing the additional challenge of terminating subtyping in this setting. In summary, we formalize conditions for preprocessing operators on types that enable simple, syntax-directed subtyping relations to capture additional desired subtyping relationships, while still retaining decidability.

14:30-14:50PreFab: a language for secure open applicationsOwen ArdenDetails

Open applications are distributed applications with rich interfaces that can be extended and executed across administrative domains. Web services with APIs, online games with mods, and federated websites like health insurance exchanges are all examples of open applications. Because open applications blur the boundaries between trusted and untrusted components, traditional approaches to security are inadequate.

To address this shortfall, we are developing PreFab, a language that provides compositional security for open applications using information flow control. PreFab is based on the Flow-Limited Authorization Model (FLAM), a new model for information flow security designed for distributed settings. In this talk I will briefly introduce FLAM, discuss the motivation and design goals of PreFab, and present initial progress.

14:50-15:20Coffee Break
15:20-15:30ModelPlex: Verified Runtime Validation of Verified CPS ModelsAndré PlatzerDetails

Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified w.r.t. the model. Otherwise, all bets are off. This paper introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model, assuming the system dynamics deviation is bounded. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions. This paper, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic.

15:30-15:40Probabilistic NetKAT½ Dexter Kozen +
½ Nate Foster

This talk will describe a new language for programming software-defined networks based on a probabilistic semantics. We extend the NetKAT language with new primitives for expressing probabilistic behaviors and enrich the semantics from one based on deterministic functions to one based on measures and measurable functions on sets of packet histories. We establish fundamental properties of the semantics, prove that it is a conservative extension of the deterministic semantics, and show that it satisfies a number of natural equations. We present case studies that show how the language can be used to model a diverse collection of scenarios drawn from real-world networks.

15:40-15:45Managing your digital lifeElisavet KozyriDetails

We discuss the problem of creating a personal information management system, which handles in a decentralized manner, the storage and distribution of information that a user daily generates. This presentation is inspired by [1].

[1] Serge Abiteboul, Benjamin Andre, Daniel Kaplan, Managing Your Digital Life, Communications of the ACM, May 2015, Vol. 58, No. 5.

15:45-15:50Fixing the tragedy of exceptionsYizhou ZhangDetails

Exception mechanisms in current languages are not well designed and do not meet the goals of an effective exception mechanism. I will talk about our work in progress on a novel exception mechanism that addresses the weaknesses of existing ones: lack of static reasoning, high performance overhead, and incompatibility with higher-order functions.

15:50-15:55MyriaStore: programming with heterogeneous consistencyMatthew MilanoDetails

Modern cloud-based application programming requires low latency and high availability across the globe, leading programmers to employ data stores with weakened consistency semantics. To make matters worse, existing web applications often have need for different consistency guarantees on objects in the same program, leading to a heterogeneous consistency semantics where the effect of "x := 5" depends heavily on where "x" is stored. In this talk, we present MyriaStore, a new framework and language which uses an information-flow type system and lightweight runtime causality tracking to provide a sane programming environment atop today's heterogenous data stores.

15:55-16:10Short talks Q & A
16:10-17:00Panel Discussion: PL research impactDexter Kozen,
Andrew Myers, and
Tom Reps
17:00-18:00Lawn games
18:00-20:00Dinner and bowling at Atlas

Validate XHTML Validate CSS
Last updated August 2015