Computing Theory Theme

This theme broadly encompases the various ways in which we understand the nature of computation: *what* is computable ("classic" computability theory, complexity theory); *how to best* compute (algorithms); *how to express* computations (programming languages); *how to understand* computations (static analyses); *how to implement* computations (compilers); computations with strong mathematical connections (cryptography).

THEORY CANAL (Rochester Theory Seminar Series).

Selected Research Projects

Computational Ramsey Theory
Ramsey theory is often regarded as the study of how order emerges from randomness. It has applications in parallel programming, approximation algorithms, game theory, geometry, number theory, and other areas of mathematics and theoretical computer science. The determination of whether many Ramsey properties hold is notoriously difficult. The goal of our research is to enhance known and develop new theoretical and computational methods solving Ramsey-type problems.

Computational Social Choice
Elections are broadly used in both human and computational settings, including a rapidly expanding range of applications in multiagent systems. It has been known since the mid-1970s (the Gibbard-Satterthwaite Theorem) that every reasonable election system has instances on which voters have an incentive to vote strategically. Computational social choice seeks to sidestep that impossibility result by making manipulation not impossible but rather computationally prohibitive.

Computational social network analysis| (CSNA)
This work combines social media, network science, sociology, and advanced computational methods to study social networks and the roles they play in organizational behavior, motivated by the belief that a better understanding of those dynamics will lead to better health, productivity, and general social welfare.

Manticore
An effort to design and implement a parallel functional programming language supporting heterogeneous parallelism (parallelism at multiple levels).| Our previous results have included novel implicitly-parallel constructs; nested schedulers with composable cancellation; lazy-tree splitting; data-only flattening; GC for multicore NUMA.| Our ongoing work is to extend the language and implementation to declarative mutable state.

MLton
A whole-program optimizing Standard ML compiler that is actively used in both industry and academia.| Our ongoing work is to whole-program compilation of next-generation language features.

Transactional Events
A novel concurrency abstraction that combines first-class synchronous message-passing events and atomic transactions and demonstrates that atomicity enhances the expressive power of message-passing.| Our ongoing work is to investigate programming idioms, efficient implementation, and fairness of transactional events.

Type-and Control-Flow Analysis
A novel program analysis that yields both control-flow (information about first-class functions) and type-flow (information about polymorphic types) and demonstrates the mutual benefit and decidability of the two flows.| Our ongoing work is to investigate efficient computation of the type- and control-flow analysis and extend the analysis to richer type systems.