Harry Mairson
Ph.D., Computer Science, Stanford University, 1984mairson at cs dot brandeis dot edu
257 Volen / (781) 736-2724
Research Interests
Other stuff---pictures, photos, poems, etc.
Slides from my invited talk at ICFP 2003, From Hilbert space to
Dilbert space: context semantics made simple. (Comments welcome.
Sorry -- this is a big file.)
Slides from my talk at GEOCAL 2006, MLL normalization and transitive closure:
circuits, complexity, and Euler tours.
Optimal evaluation: An evaluator for lambda calculus (or more broadly speaking, a functional programming language) is said to be correct and optimal if it returns a normal form whenever there is one (i.e., it never diverges by choosing to evaluate the wrong redex), and never does inessential work (i.e., copying redexes). Recently, several researchers, including Lamping, Gonthier, Abadi, Levy, and Asperti, have constructed optimal evaluators. But are they efficient?
I have examined the computational complexity of this problem via the algorithmic analysis of these proposed evaluators. In addition, this work has addressed what reasonable cost models are for the lambda calculus. In recent work, I have shown that Levy's parallel beta operation is provably not a unit cost operation in any implementation of an optimal reduction engine, and that the cost of a sequence of parallel beta steps is not bounded by any Kalmar-elementary recursive function.
Game semantics and proof structures: A denotational semantics for optimal graph reduction was given recently by Gonthier, Abadi, and Levy, where the denotation of a graph is invariant under reduction. The basic technology is an implementation of Girard's `geometry of interaction' that works as well in the context of linear logic and proof nets, explaining the incremental duplication of boxes. I am currently working on connecting the dots between this machinery and the recent work on game semantics and full abstraction.
Expressibility and typed lambda calculus: I recently developed a new proof of a famous theorem of Richard Statman, that deciding equivalence of the normal forms of two simply typed lambda terms is not Kalmar-elementary. This new proof uses basic programming insights about computing with representations of inductive data types. The insights of the proof have been extended to treat embeddings of query languages in typed lambda calculus, and to analyze the computational expressiblity of order-bounded fragments of typed lambda calculus.
Polymorphic types and type inference: The notion of polymorphic data types is one of the outstanding features of modern functional programming languages. I have studied the computational complexity of type inference for ML, showing that exponential time is required, and have extended this work to provide exponential lower bounds for System F, the polymorphic typed lambda calculus, and nonelementary bounds for Girard's Fw. The analysis has given particular insight into the complexity of higher-order unification, as well as the cost of sophisticated typing features in prototype programming languages.
Data types, subtyping, and type coercion: These topics play a crucial role in the implementation of records in typed and object-oriented programming languages. I have studied the interpretation of types as programming specifications for records, objects, and other constructs, showing how their relationship can be formalized in the calculus of constructions, a higher order logic. The analysis shows how proving theorems about programs can simultaneously be used to automatically derive low level implementations, provide a semantics for the language, and be used to derive theorems about program behavior. Subtyping relations between data types can be computationally analyzed to synthesize underlying coercion functions.
Logic and deductive databases: It has been recognized since the early 1980s that first-order database query languages are lacking in expressive power. This insight lead to the investigation of many higher-order query languages, in particular Datalog, the language of logic programs without function symbols. This language augments relational queries with a form of recursion. Recursive applications of Datalog rules make queries hard to evaluate: those without recursion, called bounded queries, can be evaluated in NC. I have worked on the problem of detecting boundedness, in an attempt to delineate the boundary (with respect to arity, number of rules, etc.) between the decidable and the undecidable.