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 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
NOV 28 Thanksgiving
DEC 12 Cancelled for Steve Awodey
DEC 12 Jeremy Siek The Essence of Closure Conversion Andrew Kent
DEC 19 Finals Week

Talk Abstracts

Sep 5: Derailer: Interactive Security Analysis for Web Applications

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.

Sep 12: Typed Clojure in Practice

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.

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.

Oct 24: A compiler for the Gradually-Typed Lambda Calculus

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.

Oct 31: Pycket; an implementation of Racket in RPython

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.

Nov 07: MACE: Detecting Privilege Escalation Vulnerabilities in Web Applications

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.

Nov 14: An Introduction to Dependently Typed Racket

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.

Nov 21: A combinator library for MCMC sampling

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.

Dec 12 : The Essence of Closure Conversion

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

Archive

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

 
talks.txt · Last modified: 2015/01/08 18:38 by cswords
Valid XHTML 1.0 Transitional