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||A compiler for the Gradually-Typed Lambda Calculus||Edward Amsden||OOPSLA|
|OCT 31||Spenser Bauman||Pycket; an implementation of Racket in RPython||Jaime Guerrero|
|NOV 07||Prasad Naldurg||MACE: Detecting Privilege Escalation Vulnerabilities in Web Applications||N/A|
|NOV 14||Andrew Kent||An Introduction to Dependently Typed Racket||Eric Holk|
|NOV 21||Praveen Narayanan||A combinator library for MCMC sampling||Mike Vollmer|
|DEC 12||Cancelled for Steve Awodey|
|DEC 12||Jeremy Siek||The Essence of Closure Conversion||Andrew Kent|
|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.
Speaker: Andre Kuhlenschmidt
There are still many open problems in gradual typing. While there seems to be a fairly common static semantics the Gradually-Typed Lambda Calculus, there are a myriad of dynamic semantics all aimed at solving various problems that occur when you start mixing static and dynamic types. I will talk informally about the motivations for various dynamic semantics, explain how they relate to and differ from one another, and talk about open problems with each of them. I will then introduce the compiler that I am working on for the GTLC and my hopes for what we may learn from it.
Speaker: Spenser Bauman
While object-oriented languages often make use of advanced just-in-time compilers for fast execution, functional languages typically rely on ahead of time compilers. Currently, there are no good JIT compilers for the Scheme family of languages, despite their successful application to other dynamic languages. In this talk, I will present Pycket; an implementation of Racket in RPython which makes use of the meta-tracing JIT infrastructure used by the Pypy project. The goal of Pycket is to provide a fast Racket implementation which can elide the overhead of traditionally difficult features like continuations, multiple return values, and Racket's contract system.
Speaker: Prasad Naldurg
We explore the problem of privilege escalation in web applications, vulnerabilities that are typically caused by missing or incorrect authorizations. In the absence of an access control policy specification in these applications, our key insight is to compute what we call the authorization state associated with each access request, using program analysis. Checking this computed state for correctness and consistency across different access requests helps us uncover vulnerabilities that can be exploited as privilege escalation attacks. We implement our techniques in MACE, a tool that works on large codebases, and discovers serious vulnerabilities in 5 out of 7 web applications that were previously unknown, replacing weeks of human effort and manual code inspection.
Speaker: Andrew Kent
Typed Racket is a gradually typed dialect of Racket that seeks to accommodate common typed-based reasoning used in untyped languages, while requiring few changes to the code itself. However, thus far Typed Racket has only supported formally reasoning about relatively simple types. In this informal talk I will briefly review the base calculus for this system (λTR) and illustrate how decidable dependent types (such as those found in Dependent ML) are a natural extension to the calculus.
Speaker: Praveen Narayanan
In this talk I will present an initial version of a Haskell library designed to ease the construction and use of MCMC samplers. I will first introduce the MCMC method and motivate its application on a concrete example - the Gaussian Mixture Model (GMM). I will then describe an MCMC sampler for a GMM, and show how this sampler can be made more modular by using combinators from the library. The goal is to convince the audience of the benefits of applying paradigms such as higher order functions and lazy evaluation to the domain of MCMC sampling. No prior experience with MCMC samplers is required, and questions are strongly encouraged.
Speaker: Jeremy Siek
The interaction between lexical scoping of variables and first-class functions, as found in all functional programming languages, is rather subtle and interesting, especially if you want to compile the language to assembly code. For some reason, computer architects have yet to include first-class functions with lexical scoping in modern computers! In this talk I'll try to capture the essence of compiling from a language with lexical scoping and first-class functions to a language without lexical scoping (but unusually, still with first-class functions).