PhD Student in the Computer Science Department- CMU

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

Abstract:

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.

Bio:

Nicolas is a third-year PhD student in CSD

Principles
of Programming Seminars