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.

Fall 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 (though we avoid peanuts due to allergies).

Date Speaker Title Food Notes
SEP 5 Joe Near Derailer: Interactive Security Analysis for Web Applications Rob Zinkov ICFP
SEP 12 Ambrose Bonnaire-Sergeant Typed Clojure in Practice Andre Kuhlenschmidt
SEP 19 Chris Wailes Introduction to Topologically Aware Load Balancing Peter Fogg
SEP 26 Ed Amsden Type-Directed Editing Praveen
OCT 03 Matteo Cimini A Method for Proving Congruence of Bisimilarity in Nominal SOS Jason Hemann
OCT 10 Eric Holk Region-based Memory Management for GPU Programming Languages Ambrose BS
OCT 17 Mike Vitousek Design and evaluation of gradual typing for Python Cameron Swords
OCT 24 Andre Kuhlenschmidt Edward Amsden OOPSLA
OCT 31 Spenser Bauman Jaime Guerrero
NOV 07 Aaron Hsu Johanna Hsu
NOV 14 Andrew Kent Eric Holk
NOV 21 Tim Zakian Mike Vollmer
NOV 28 Thanksgiving
DEC 05 Jeremy Siek Andrew Kent
DEC 12 Praveen / Mike Vollmer Mike Vitousek
DEC 19 Finals Week

Talk Abstracts

Sep 5: Derailer: Interactive Security Analysis for Web Applications

Speaker: Joe Near

Abstract:

Derailer is an interactive tool for finding security bugs in web applications. Using symbolic execution, it enumerates the ways in which application data might be exposed. The user is asked to examine these exposures and classify the conditions under which they occur as security-related or not; in so doing, the user effectively constructs a specification of the application’s security policy. The tool then highlights exposures missing security checks, which tend to be security bugs.

We have tested Derailer’s scalability on several large open-source Ruby on Rails applications. We have also applied it to a large number of student projects (designed with different security policies in mind), exposing a variety of security bugs that eluded human reviewers.

Sep 12: Typed Clojure in Practice

Speaker: Ambrose Bonnaire-Sergeant

Abstract:

Typed Clojure is an optional type system for Clojure. Typed Clojure is being used in production systems to help programmers verify, document and design correct Clojure code. In this talk, we introduce the goals of Typed Clojure and discuss how effectively Typed Clojure works in practice. We give an overview of the kinds of problems being solved today with Typed Clojure, and where your Clojure projects might benefit from a type system like it.

Sep 19: Introduction to Topologically Aware Load Balancing

Speaker: Chris Wailes

Topologically aware load balancing (TALB) was originally intended to address the needs of a few high performance scientific computing researchers in the 80s who had access to “massively parallel” machines (between 8 and 1024 processors at the time). Now, with top of the line supercomputers having upwards of 1.5 million nodes and desktop computers quickly gaining cores by the dozens, TALB has become relevant to a much wider range of applications and users. In this talk I will present a brief history of the field, the three main classes of algorithms used, and some of the challenges facing the field. Lastly I will present some of my ongoing research.

Sep 26: Type-Directed Editing

Speaker: Ed Amsden

I will present a set of editing actions on terms in the simply-typed lambda calculus. These actions preserve the well-typedness of terms, and allow the derivation of any well-typed term beginning with any other well-typed term, without resorting to metavariables or other forms of placeholders. By the time of the talk I hope to have proved that any well-typed term can be constructed from the unit term, and that all editing actions preserve well-typedness.

Oct 03: A Method for Proving Congruence of Bisimilarity in Nominal SOS

Speaker: Matteo Cimini

Structural Operational Semantics (SOS) is one of the most natural ways for providing programming languages with a formal semantics. In this talk, we focus on Nominal SOS, a formalization of SOS with explicit syntax and primitives for the specification of languages with binders, as lambda-calculus and pi-calculus. In SOS, bisimilarity is typically the most suitable equivalence relation over programs. We offer a syntactic method for proving that bisimilarity is a congruence for languages defined in Nominal SOS, i.e. that bisimilarity is preserved by all the operators of the language being defined. We show the applicability of the method by recovering classic results, most notably that Sangiorgi’s open bisimilarity is a congruence for pi-calculus. (Remark: This is a nearly finished, but unfinished work.)

Oct 10: Region-based Memory Management for GPU Programming Languages: Enabling Rich Data Structures on a Spartan Host

Speaker: Eric Holk

Graphics Processing Units (GPUs) can effectively accelerate many applications, but their applicability has been largely limited to problems whose solutions can be expressed neatly in terms of linear algebra. Indeed, most GPU programming languages limit the user to simple data structures–typically only multidimensional rectangular arrays of scalar values. Many algorithms are more naturally expressed using higher level language features, such as algebraic data types (ADTs) and first class procedures, yet building these structures in a manner suitable for a GPU remains a challenge. We present a region-based memory management approach that enables rich data structures in Harlan, a language for data parallel computing. Regions enable rich data structures by providing a uniform representation for pointers on both the CPU and GPU and by providing a means of transferring entire data structures between CPU and GPU memory. We demonstrate Harlan’s increased expressiveness on several example programs and show that Harlan performs well on more traditional data-parallel problems.

Oct 17: Design and evaluation of gradual typing for Python

Speaker: Michael Vitousek

I will discuss Reticulated Python, a system for experimenting with gradual-typed dialects of Python. It is syntactically identical to Python 3 but gives static and dynamic semantics to the type annotations already present in Python 3. Reticulated Python consists of a typechecker and a source-to-source translator from Reticulated Python to Python 3. Using Reticulated Python, we evaluated a gradual type system and three approaches to the dynamic semantics of mutable objects: the traditional semantics based on Siek and Taha (2007) and Herman et al. (2007) and two new designs. We evaluated these designs in the context of several third-party Python programs.

Archive

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

 
talks.txt · Last modified: 2014/10/20 08:48 by cswords
Valid XHTML 1.0 Transitional