Indiana University Bloomington

PL Colloquium Series

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.

Spring 2014 Schedule

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

Date Speaker Title Food Notes
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 Ed Amsden Eric Holk
Apr. 18 Aaron Hsu J0hanna Hsu
Apr. 25 Sam Tobin-Hochstadt Praveen Narayanan
May. 02 Rob Zinkov Matteo Cimini

*: In LH008

Talk Abstracts

Jan 17: Talk Sign-up Meeting / Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars

Speaker: Lindsey Kuper

Abstract:

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.

Jan. 31: Towards a Computational Account of Homotopy Type Theory

Speaker: Zach Sparks

Abstract:

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.

Feb. 12: Monotonic References for Gradual Typing

Speaker: Jeremy Siek

Abstract:

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.

Feb. 21: Linear Types: Out of the Ivory Tower and Into the Trenches

Speaker: Chris Wailes

Abstract:

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.

Archive

For older talks, please refer to the announcements in the pl-wonks-l archives (accessible to list subscribers).

 
talks.txt · Last modified: 2014/04/07 13:39 by arcfide
Valid XHTML 1.0 Transitional