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.