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||Ed Amsden|
|Mar. 07*||Jason Hemann||Chris Wailes|
|Mar. 14||Lindsey Kuper||Zach Sparks|
|Mar. 21||~*~ SPRING BREAK ~*~|
|Mar. 28||Amr Sabry||Lindsey Kuper|
|Apr. 04||Michael Vitousek||Cameron Swords|
|Apr. 11||Aaron Hsu||J0hanna Hsu|
|Apr. 18||Ed Amsden||Eric Holk|
|Apr. 25||Sam Tobin-Hochstadt||Praveen Narayanan|
|May. 02||Rob Zinkov||————|
*: 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.