Our weekly meeting and talk series, known affectionately as “PL-wonks”, is open to everyone interested in discussing programming languages research happening here at IU. Our talks include original research, experience reports, and tutorials. We also sometimes present papers from the literature that we're interested in.
Unless otherwise noted, PL talks happen every Friday at 4:15pm in Lindley Hall Room 101.
All are welcome to attend.
We have a tradition of baking cookies and other treats for our meetings (and there is usually something vegan-friendly and we avoid peanuts due to allergies).
|Jan. 17||Scheduling / Lindsey Kuper||Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars||Andre Kuhlenschmidt|
|Jan. 24||Cancelled in favor of POPL|
|Jan. 31||Zach Sparks||Towards a Computational Account of Homotopy Type Theory||Michael Vitousek|
|Feb. 07||Cancelled in favor of this week's job talk|
|Feb. 12||Jeremy Siek||Monotonic References for Gradual Typing||Andre Kuhlenschmidt||At 1:00 (Note Special Time and Date)|
|Feb. 21||Chris Wailes||Linear Types: Out of the Ivory Tower and into the Trenches||Tim Zakian|
|Feb. 28||Eric Holk||Towards a Parallel CSS Selector Matching Algorithm in Harlan||Ed Amsden|
|Mar. 07*||Jason Hemann||Recovering and enhancing miniKanren||Chris Wailes|
|Mar. 14||Lindsey Kuper||LVars: Lattice-based Data Structures for Deterministic Parallel and Distributed Programming||Zach Sparks|
|Mar. 21||~*~ SPRING BREAK ~*~|
|Mar. 28||Amr Sabry||Conway Games||Paul Ojanen|
|Apr. 04||Michael Vitousek||Reticulated Python: Gradual Typing for Python||Cameron Swords|
|Apr. 11||Ed Amsden||Type-Directed Editing||Eric Holk|
|Apr. 18||Aaron Hsu||A Few of My Favorite Things: Compilers and APL||J0hanna Hsu|
|Apr. 25||Sarah Loos||Verifying Hybrid Systems with Automated Theorem Provers||Praveen Narayanan|
|May 02||Rob Zinkov||Probabilistic Programming for the PL researcher||Matteo Cimini|
|May 09||Carl Eastlund||Modules and Metaprogramming for the ACL2 Theorem Prover||Lindsey Kuper|
*: In LH008
Speaker: Lindsey Kuper
Deterministic-by-construction parallel programming models offer the advantages of parallel speedup while avoiding the nondeterministic, hard-to-reproduce bugs that plague fully concurrent code. A principled approach to deterministic-by-construction parallel programming with shared state is offered by LVars: shared memory locations whose semantics are defined in terms of an application-specific lattice. Writes to an LVar take the least upper bound of the old and new values with respect to the lattice, while reads from an LVar can observe only that its contents have crossed a specified threshold in the lattice. Although it guarantees determinism, this interface is quite limited.
We extend LVars in two ways. First, we add the ability to “freeze” and then read the contents of an LVar directly. Second, we add the ability to attach event handlers to an LVar, triggering a callback when the LVar's value changes. Together, handlers and freezing enable an expressive and useful style of parallel programming. We prove that in a language where communication takes place through these extended LVars, programs are at worst quasi-deterministic: on every run, they either produce the same answer or raise an error. We demonstrate the viability of our approach by implementing a library for Haskell supporting a variety of LVar-based data structures, together with a case study that illustrates the programming model and yields promising parallel speedup.
Speaker: Zach Sparks
Homotopy type theory (HoTT) has recently become a popular topic of discussion in certain circles in PL academia, drawing from research in programming languages, topology, and category theory. Its main focus is equality of elements, and specifically looking at paths between equal objects. Unfortunately, they currently must postulate that types have a path between them (ie, are equal) exactly when there is an equivalence between them. This axiom—known as the univalence axiom—is aesthetically unpleasing to some, and also causes difficulties when trying to interpret HoTT as a programming language with computational rules.
The Pi programming language is a language in which all computations are reversible. This provides a natural setting for reasoning about equality, since the type of programs in Pi forms an equivalence relation by design. Together with Amr Sabry and Jacques Carette, I have been working on a computational alternative to HoTT, using Pi as a basis. In this talk, I will introduce the basics of both HoTT and Pi, explain the problems with HoTT, and discuss our novel approach to solving them.
Speaker: Jeremy Siek
Gradual type systems enable the use of both static and dynamic type checking within a single program. In such systems, it is important to enable the seemless transfer of data between the static and dynamic parts of the program while at the same time ensuring that the dynamic parts do not invalidate the invariants assumed by the static parts. In particular, dereferencing something of static type 'reference to integer' should return an integer value. To date, the only approach that ensured this invariant also induced extra run-time overhead in every dereference, both in dynamically and statically typed code. In this talk I present a new point in the design space, monotonic references, that removes the run-time overhead from dereferencing statically-typed references. I also give an overview of our proof of type safety in Isabelle, which was non-trivial because this design utilizes strong (type-changing) updates to the heap.
Speaker: Chris Wailes
Taking software techniques and tools that were developed in an academic setting and making them available and useful to the wider world of software developers can be a difficult task. This is especially true when one is targeting a language like C++. In such settings pointers can complicate any analysis that isn't specifically designed to handle them and large bodies of existing code must remain working with little or no modification. One must also consider the number of false positives that will be generated by the tool or analysis, as well as the effort required by the developer to use it. Both of these factors can significantly impact the adoption of a potential tool. This talk will discuss specific issues encountered while developing a linear types analysis for C++. I will review design decisions that we made and present the system as it currently stands in Clang 3.4.
Speaker: Eric Holk
Harlan is a new programming language enabling functional programming on GPUs and similar data parallel hardware. Though Harlan has a rich set of features, including first class procedures and algebraic data types, it has not been clear what to do with these things. I will present efforts to implement a parallel CSS selector matching algorithm in Harlan and show how Harlan’s high level features support the development of such an algorithm.
Speaker: Jason Hemann
miniKanren is a relational programming language designed with purity and portability in mind. Recently, we developed a small language kernel, microKanren , which is somewhat low-level but powerful enough to perform actual relational-programming tasks. We demonstrate here a miniKanren implementation with microKanren as its core, provide some rough performance comparisons, and describe a new implementation of unify.
Speaker: Lindsey Kuper
Parallel programming is notoriously difficult. A fundamental reason for this difficulty is that unpredictable interactions between parallel tasks lead to subtle, hard-to-reproduce nondeterministic bugs. Deterministic-by-construction parallel programming models promise freedom from those bugs, but to do so they must sharply restrict the sharing of state between parallel tasks. Shared state, if it is allowed at all, is typically restricted to a single type of shared data structure, such as single-assignment locations or blocking FIFO queues.
In this talk, I'll describe my work on a new model for guaranteed-deterministic parallel programming based on lattice-based data structures, or LVars. LVars generalize existing single-assignment models to allow multiple assignments that are monotonically increasing with respect to a lattice, making possible a more general form of communication between tasks. LVars ensure determinism by allowing only monotonic writes and “threshold” reads that block until a lower bound is reached, preventing the order of writes from being observed.
After presenting the basic LVars model, I'll discuss several extensions to the model that enable an expressive and useful style of parallel programming while maintaining the determinism guarantee. I'll show how these extensions are realized in practice in LVish, a library for guaranteed-deterministic parallel programming with LVars. Finally, I'll discuss my ongoing work on the relationship between LVars and conflict-free replicated data types for eventually consistent distributed systems.
Speaker: Amr Sabry
Our recent work on using “conservation of information” as a foundational principle of computation requires a highly symmetrical computational model. In particular, the type structure of such language includes duals to conventional sum and product types, the so-called negative and fractional types. Although we have a reasonable operational understanding of computations involving such types, previous attempts to find an adequate semantic model have failed. A very recent investigation shows, however, that the theory of games founded by Conway in the 70s may have the right ingredients for our desired model. The current status of this investigation is speculative at best, so this will a rather informal talk that aims to introduce the basic definitions of our computational model and of Conway games and argue that there is a good match without providing any concrete results.
Speaker: Michael Vitousek
Combining static and dynamic typing within the same language, i.e. gradual typing, offers clear benefits to programmers. However, many open questions remain regarding the semantics of gradually typed languages, especially concerning the integration of gradual typing with existing languages. I will discuss Reticulated Python, our lightweight system for experimenting with gradual-typed dialects of Python. Using Reticulated Python, we evaluated a gradual type system that features structurally-typed objects and type inference for local variables. I will discuss two dynamic semantics for casts which we implemented and evaluated in Reticulated Python: one based on proxies and one design that instead uses statically-inserted, use-site checks.
Speaker: Edward Amsden
A programmer's primary tools are still a text editor and a compiler or interpreter. Certainly, today's text editors have been enhanced with impressive capabilities for managing, comprehending, refactoring, and re-using code. But what if our editing actions followed the semantics of our languages? We know that type-safety guarantees that many programming errors will be caught before the program is run. But can we give the programmer the comfort that all of his editing operations produce valid programs? Might we be able to *offer* correct actions to the programmer, thus avoiding the frustration of following a software suggestion that turns out to be incorrect, and without explanation? Can we make the process of editing programs high-level as we make our languages high-level?
I present the direction of my research into type-directed editing, and in particular I propose “wearing the hair shirt”, attempting to program using only type-directed edits in order to understand the benefits and difficulties, and to understand what tools and editing capabilities are necessary for type-directed editing to be a useful programming UI model.
Speaker: Aaron Hsu
This will be an informal and hopefully fun exploration of array programming and compilation. I hope to tell an entertaining story of my foray into array programming, and give people a feel of what it's actually like using array programming for “real work”; that is, what it's like using array programming as a general purpose programming language in a domain not usually considered an array programming domain: compilers. I'll cover some of the techniques and thoughts that distinguish array programming at scale from traditional functional programming languages, as well as some of the results of my efforts, including preliminary benchmarks of my APL compiler.
Speaker: Sarah Loos
Formal verification and theorem proving have been used successfully in many discrete applications, such as chip design and verification. However, computation is not confined to the discrete world of desktop computing. Increasingly, we depend on discrete software to control safety-critical components of continuous physical systems (for example, adaptive cruise control in cars and collision avoidance in aircraft). It is vital that these hybrid (discrete and continuous) systems behave as designed, or they will cause more damage than they intend to fix. In this talk, I will present several challenges associated with verifying hybrid systems and how we can usedifferential dynamic logic and its proof calculus to ensure safety for hybrid systems under a continuously infinite range of circumstances.
In addition to covering the theoretical foundations for deductive verification of hybrid systems, I will discuss some of the practical uses of our verification tools: KeYmaera and KeYmaeraD. These tools have been used to verify a class of distributed collision avoidance controllers designed to work in environments with arbitrarily many aircraft. We prove that the controllers never allow the aircraft to get too close to one another, even when new planes approach an in-progress avoidance maneuver that the new plane may not be aware of. Because these safety guarantees always hold, the aircraft are protected against unexpected emergent behavior, which simulation and testing may miss.
Speaker: Rob Zinkov
Bayesian inference tasks and machine learning in general we are often inferring some latent quantity given some observed data and a theory for how this latent quantity generated this data. The idea behind probabilistic programming languages is that this theory of how the data was generated is best expressed as a programming language. In this talk, I will introduce a denotational semantics for one such language based on measures which can be understood as unnormalized probability distributions. I will then introduce an operational semantics based on Markov-Chain Monte Carlo (MCMC) sampling. Finally, I will show that these two semantics are not isomorphic and mappings between the two do not preserve algorithmic performance. I will highlight applications that range from outlier detection to clustering algorithms to predicting who will run a game of tug-of-war.
Speaker: Carl Eastlund
The ACL2 theorem prover provides formal reasoning tools for a pure, first-order subset of Common Lisp. Companies such as AMD, IBM, and Rockwell Collins use ACL2 to model and verify critical hardware and software artifacts. Unfortunately, ACL2 is a small, simple language, while the models it verifies are large and complex. ACL2 has a few tools up its sleeve to tame this complexity: macros, packages, and encapsulation. Unfortunately, these tools each come with their own pitfalls. Unhygienic macros are a metaprogramming tool that is oblivious to the scope of names. Common Lisp's package system provides namespace management in a way that causes more problems than it solves. And ACL2's encapsulation mechanism defines logical abstractions that prevent a model from being executed, are cumbersome to instantiate, and tend to increase code duplication rather than decreasing it.
For my PhD dissertation, I designed and implemented a language called “Refined ACL2” that resolves these problems by equipping the logic and core language of ACL2 with the hygienic macros of Racket and the module system of ML. Racket's hygienic macros observe lexical scope, allowing complex language extensions while avoiding pitfalls such as unintended capture. The ML module system provides both namespace management and logical abstraction, without the difficulties of Common Lisp's packages, and while remaining both executable and easy to instantiate.