Talks

Linear-Log Time Control-Flow Analysis with Flow-Sensitivity and Predicate-Awareness

• Venue: POPL Student Presentation Session, January 27, 2011.
• Links: Slides

Control Flow Analysis

• Venue: Algorithms Reading Group, Indiana University, September 20, 2010.

Scrap Your Zippers: A Generic Zipper for Heterogeneous Types

• Venue: Programming Languages Seminar, Indiana University, September 17, 2010.
• Links: Paper

• Abstract:

  The zipper type provides the ability to efficiently edit tree-shaped data in a purely functional setting by providing constant time edits at a focal point in an immutable structure. It is used in a number of applications and is widely applicable for manipulating tree-shaped data structures.

  The traditional zipper suffers from two major limitations, however. First, it operates only on homogeneous types. That is to say, every node the zipper visits must have the same type. In practice, many tree-shaped types do not satisfy this condition, and thus cannot be handled by the traditional zipper. Second, the traditional zipper involves a significant amount of boilerplate code. A custom implementation must be written for each type the zipper traverses. This is error prone and must be updated whenever the type being traversed changes.

  The generic zipper presented in this talk overcomes these limitations. It operates over any type and requires no boilerplate code to be written by the user. The only restriction is that the types traversed must be instances of the Data class from the Scrap your Boilerplate framework.

Control-Flow Analysis and Abstract Interpretation: Running Your Program without Running Your Program

• Venue: Programming Languages Seminar, Indiana University, October 2, 2009.

• Abstract:

  Control-Flow Analysis (CFA) allows the determination of what value a particular variable might have at run-time and is the backbone of many forms of static analysis. This talk will cover CFA and its connection to another fundamental static analysis, Abstract Interpretation (AI). Also the CFA hierarchy as well as CFA’s and AI’s relationship to type checking will be discussed.

Deriving Syntax-Case from First Principals: How to turn a name freshener into a macro expander

• Venue: Programming Languages Seminar, Indiana University, February 6, 2009.

• Abstract:

  The syntax-case macro expander represents the state of the art with regard to macro expansion systems in the Scheme community. Unfortunately the full algorithm is fairly difficult to comprehend with marks, anti-marks, shifts and contexts interacting in complicated ways. However, behind it all lies a very simple core that is obscured by layers of optimization.

  This talk will attempt to expose that simplified core algorithm by deriving a macro expander from a name freshener and a few simple principals. In the process an intuitive model for how the syntax-case expander works will be developed that is simpler than the traditional syntax-case implementation and is suitable for reasoning about typical macros a programmer write.

Verifying a Filesystem: A Successful Failure

• Venue: Programming Languages Seminar, Indiana University, April 25, 2008.
• Co-speaker with Joseph Near and Aaron Kahn
• Links: Slides (PowerPoint PDF), Project Report

• Abstract:

  The filesystems we use every day need to be among the most reliable programs on our computers, since losing data can be disastrous. The filesystems we use often go through years of testing to ensure their reliability. Despite this testing, even the most reliable of filesystems occasionally fails, resulting in lost data.

  In this talk we will present an account of our attempt to formally verify a model of a filesystem implementation similar to many popular filesystems used today. We will cover the design of our filesystem, its implementation and translation into the language of the proof assistant PVS, and our attempts to prove that translation correct. While our attempts were ultimately unsuccessful, we gained important insights into the problems associated with proving properties about programs containing side effects and serialization.

  We will also present our proposal for a new attempt to solve the problem, based on linear types. This approach simplifies the proofs of properties involving side effects and serialization through the use of a separate theory of serialization. This theory, which would apply to programs written in terms of linearly typed objects, would generate proofs for a serialized, state-based implementation from the users’s proofs correctness of the side-effect free version.

Scrapping Scrap your Nameplate

• Venue: Programming Languages Seminar, Indiana University, March 7, 2008.
• Links: Slides (OpenOffice PDF)

• Abstract:

  “Scrap your Nameplate” by James Cheney, the author of alpha-Prolog, demonstrates a method of writing nominal programing that avoids the need to write large amounts of “boilerplate” code for each user declared data type. It is written in Haskell and leverages the techniques described in “Scrap your Boilerplate”. However, it has fundamental flaws that break the pure nominal programing paradigm. This talk will give an introduction to “Scrap your Nameplate”, point out the areas where it is flawed and sketch an alternative implementation technique that avoids those flaws.

Meta-Programming in Haskell with GADTs

• Venue: Programming Languages Seminar, Indiana University, October 26, 2007.
• Links: Slides (OpenOffice PDF), Source

• Abstract:

  This talk presents work I have done on a proof-of-concept embedding of Meta-Programming directly into Haskell with an eye toward implementing typed scheme macros. It will also include an introduction to GADTs and their uses.

  A unique feature of the system presented is that it provides an implementation of the lambda calculus that is type-safe without requiring the implementation of a type checker. Instead the type system of the host language (Haskell) enforces well-typed-ness on the terms in the embedded language.

A Poet’s Musings on Efficient Computation

• Venue: Programming Languages Seminar, Indiana University, April 10, 2007.

• Abstract:

  A sort talk on ideas related to parsing mechanisms, computational complexity and some “less-obviously” related fields.

Seven at One Stroke: Results from a Cache-Oblivious Paradigm for Scalable Matrix Algorithms

• Venue: Programming Languages Seminar, Indiana University, October 19, 2006.
• Links: Paper

• Abstract:

  A blossoming paradigm for block-recursive matrix algorithms is presented that, at once, attains excellent performance measured by

  • time,
  • TLB misses,
  • L1 misses,
  • L2 misses,
  • paging to disk,
  • scaling on distributed processors, and
  • portability to multiple platforms.

  It provides a philosophy and tools that allow the programmer to deal with the memory hierarchy invisibly, from L1 and L2 to TLB, paging, and inter-processor communication. Used together, they provide a cache-oblivious style of programming.

  Plots are presented to support these claims on an implementation of Cholesky factorization crafted directly from the paradigm in C with a few intrinsic calls. The results in this paper focus on low-level performance, including the new Morton-hybrid representation to take advantage of hardware and compiler optimizations. In particular, this code beats Intel’s Matrix Kernel Library and matches AMD’s Core Math Library, losing a bit on L1 misses while winning decisively on TLB-misses.

Existential Types: How to write first class patterns in Haskell

• Venue: Programming Languages Seminar, Indiana University, September 7, 2006.