Nicolas Feltman
PhD Student in the Computer Science Department- CMU

Creating Data Structures from Algorithms by Stage-splitting a Modal Language

Many algorithms operate by first building a searchable index structure over some data and then repeatedly performing queries on that index.  It is often observed that the form and invariants of such intermediate data structures (e.g. a list sorted by quicksort) mirror the design of a divide-and-conquer algorithm (quickselect).  Our goal is to automatically derive the former from the latter.  We accomplish this by writing the divide-and-conquer algorithm in a two-stage lambda calculus (corresponding to non-branching temporal logic) and running a stage-splitting algorithm to factor this one two-stage program into two one-stage programs.  We also discuss possible applications of our lambda calculus in the design of domain-specific languages, wherein the stage-splitting algorithm becomes part of the compilation process.

Nicolas is a third-year PhD student in CSD

Thursday, May, 1st, 2014
3:00 PM
Gates & Hillman Centers 6501

Principles of Programming Seminars