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 (though we avoid peanuts due to allergies).
|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|
|DEC 05||Jeremy Siek||Andrew Kent|
|DEC 12||Praveen / Mike Vollmer||Mike Vitousek|
|DEC 19||Finals Week|
Speaker: Joe Near
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.
Speaker: Ambrose Bonnaire-Sergeant
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.
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.
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.
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.)
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.
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.