Tasks

• Goal. Each of you will either select a topic from the list below or suggest a topic by yourself, where each topic consists of several papers. You will then complete three tasks. Ideally, you would study not only the listed papers (including appendices and proofs), but also other relevant papers (e.g., those cited by, or citing, the listed papers).
• Task 1: Proposal Presentation (10%). Give a 5-minute presentation in English that:
  • Introduces the problem investigated in the selected papers.
  • Outlines a plan for an in-depth study.
• Task 2: Final Presentation (20%). Give a 30-minute presentation that explains:
  • The main problem with its motivation and significance.
  • The main results with their strengths and weaknesses.
  • Concrete follow-up research questions and any preliminary results if available.
  • Note: Each presentation will be followed by a 5-minute Q&A session.
• Task 3: Final Report (20%). Write a 5-page report that includes:
  • A summary of the selected papers (which may be from outside the provided list), including some mathematical details.
  • A discussion of their significance, strengths, and weaknesses.
  • A description of concrete follow-up research questions, and any preliminary results (either theoretical or empirical) on the questions if possible.
  • Note: References, figures, and tables do not count toward the 5-page limit.

Venues

• CS Theory & Math: STOC, FOCS, SODA / JACM, Ann. Math.
• Computer Arithmetic: ARITH / TOMS, TC.
• Programming Languages: POPL, PLDI, OOPSLA, LICS, CAV / TOPLAS.
• Machine Learning: NeurIPS, ICML, ICLR, COLT, AISTATS / JMLR.
• Security: CCS, S&P, Security.

Topics

Numbers (4+1)

• Implementing computable reals (Android calculators, etc.)
  • Towards an API for the Real Numbers [PLDI 2020, Boehm] (Google)
  • Arbitrary Precision Real Arithmetic: Design and Algorithms [JLP 2005, Ménissier-Morain]
  • Exact Real Computer Arithmetic With Continued Fractions [TC 1990, Vuillemin]
  • The iRRAM: Exact Arithmetic in C++ [CCA 2000, Müller] (iRRAM)
  • Additional Papers
• Deciding logical formulas over computable reals ($\delta$-decidability)
  • Satisfiability modulo ODEs [FMCAD 2013, Gao+]
  • δ-Complete Decision Procedures for Satisfiability over the Reals [IJCAR 2012, Gao+]
  • Delta-Decidability over the Reals [LICS 2012, Gao+]
• + Real computation and complexity theory
  • Complexity and Real Computation (Chapter. Complexity Classes over the Reals).
  • The Existential Theory of the Reals as a Complexity Class: A Compendium.