Theoretical Aspects of Computing

This area broadly encompases the various ways in which we understand the nature of computation:

• What is computable - 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

• Arthur Azevedo de Amorim
• Ivona Bezáková: algorithm design, counting and sampling of graph structures, evaluation of partition functions of spin systems, analysis of Markov chains, hardness of approximation
• Varsha Dani
• Matthew Fluet: functional programming, compiler construction, parallelism and concurrency, program analysis, type systems
• Edith Hemaspaandra
• Richard Lange
• Stanisław Radziszowski: combinatorial computing, cryptography
• Carlos Rivero: graph theory
• Haibo Yang

• Angelina Brilliantova (advisor: Ivona Bezáková)
• Zohair Raza Hassan (advisors: Edith Hemaspaandra & Stanisław Radziszowski)
• Narayanan Asuri Krishnan (advisor: Carlos Rivero)
• Hannah Miller (advisors: Ivona Bezáková and Edith Hemaspaandra)
• Anastasiia Vitko (advisors: Varsha Dani & Ivona Bezáková)
• Dongyu Wu (advisor: Arthur Azevedo de Amorim)

• AI and Economics: Through the integration of artificial intelligence (AI), economics, and computation this project investigates novel solutions for socially desirable outcomes in dynamic environments. With the advent of online platforms, economic theory emerges as a fundamental approach to promote desirable social properties of efficiency, fairness, and truthfulness in a variety of domains such as shift scheduling, course registration, cloud computing, and crowdsourcing. These new applications are beyond the scope of classical economic theory and market design. Complex scenarios involving changing preferences, dynamic populations, and online items require novel, practical, and scalable solutions. This project aims at investigating various economic and social properties from algorithmic and computational lenses, and provide theoretical boundaries for such algorithms.
• Algorithmic Fair Division and Matching Theory: this field is a branch of mechanism design that concerns with developing efficient algorithms for resource allocation that guarantee optimal outcomes while incentivizing truthful behavior. Several real-life problems are concerned with matching two disjoint sides of the market to one another based on agents’ preferences or with allocation of resources among (possibly) self-interested agents in a fair manner. This project aims at investigating various social properties of matching mechanisms to 1) provide theoretical analysis of matching mechanisms in various settings, 2) devise new algorithms through AI techniques for reasoning over incomplete preferences, and 3) provide empirical evaluations of the proposed algorithms.
• Automated Feedback in Computing Theory: Understanding computing theory concepts is challenging, yet it is a very important part of computer science education. As a first step, students learn about various models of computation such as finite and push-down automata, various types of grammars, and Turing machines. To understand more complex computational issues, students need to fully comprehend the possibilities and limitations of these models. Many students struggle with these concepts due to their mathematical nature. JFLAP is an excellent and widespread tool that provides a way for students to interact with these concepts. For example, it lets students design their automaton graphically on a computer and it steps through the computation of the automaton on a given input. However, if asked to design an automaton for a given language, the students can only "run" their automaton on some inputs. Even if the automaton behaves correctly on these inputs, it might still be incorrect on other inputs. In such a case, students typically learn of their mistakes much later, as grading these assignments is especially time consuming. The goal of this proposal is to automatically generate immediate feedback that determines whether a solution is correct, and if not, it will provide a "witness" of the incorrectness (for example, an input on which the automaton fails). The tool will also estimate the "quality" of the solution, including a score indicating how far the solution is from being correct, which can be used for automated grading.
• Automated Feedback in Programming Assignments: Student interest in computer science courses is rapidly increasing, putting strain on departments and instructors to offer a quality education. Providing effective personalized feedback to students is a critical part of this process, but the limited number of qualified instructors and large student enrollments make providing feedback a challenge. In addition, promoting responsive teaching informed by the analysis of student submissions allows better student engagement. Our goal is to develop a new teaching platform to automatically propagate feedback to a large body of students and to assist instructors with programming assignments in computer science courses. In addition, the new teaching platform aims to help instructors understand collective strengths and weaknesses of students in their courses based on their assignment submissions and explicitly promote responsive teaching. The teaching platform will create program dependence graphs from student submissions that combine control and data flows for Java and Python programs. Such graphs will enable the platform to cluster similar student submissions using graph alignment, and to detect semantic expected code patterns using subgraph mining for providing feedback to students. Analytics over the data managed by the platform will help promote responsive teaching and help instructors understand students' needs.
• 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.
• Manticore: A research effort to design and implement a heterogeneous parallel functional programming language that targets commodity multicore and shared-memory multiprocessors.  Our previous results have included novel implicitly-parallel constructs; nested schedulers with composable cancellation; lazy-tree splitting; data-only flattening; GC for multicore NUMA; partial aborts for software transactional memory.  Our ongoing work is to extend the language and implementation to declarative mutable state.
• MLton: An open-source whole-program optimizing compiler for Standard ML that is actively used in both industry and academia.  Our ongoing work is to explore 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).  Our previous results have demonstrated the mutual benefit and decidability of the two flows and developed an efficient computation of the type- and control-flow analysis for SystemF.  Our ongoing work is to extend the analysis to richer type systems.
• Counting and sampling of discrete structures: Optimization problems aim to find the best answer according to some criteria; a well-known example is the problem of finding the shortest path in a graph. Counting problems aim to compute the total number of feasible solutions, such as the total number of paths, or the total number of shortest paths. For many natural problems the number of feasible solutions is exponentially large and the counting problem is #P-complete. In such cases, does there exist an approximation algorithm? Or is it also hard to approximate the answer? We investigate several algorithmic techniques for counting problems, including Markov Chain Monte Carlo that estimates the count via sampling.
• Partition functions of spin systems: Many counting problems can be phrased as spin systems, where each vertex is assigned a spin from a set of predetermined values. Each possible configuration of spins has an associated weight, and the (weighted) counting problem aims to compute the sum of the weights of all configurations. This quantity is also known as the partition function, a normalizing factor that converts the weights into a probabilistic distribution over the configurations. Partition functions are heavily used in a number of areas ranging from statistical physics, machine learning, and computer vision.

• Multiagent Systems Lab [Hosseini]: https://www.cs.rit.edu/~hho/mas
• Graph-Oriented AppLications Lab [Rivero]: https://www.cs.rit.edu/~crr/goal/