POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Mon 20 Jan 2025 09:00 - 10:00 at Duck, Duck Goose - Session 1

Complex reasoning problems are most clearly and easily specified using logic rules, but require recursive rules with aggregation such as count and sum and more for practical applications. Unfortunately, the meaning of such rules has been a significant challenge, with many disagreeing semantics, implemented in different classes of solvers and rule engines.

This talk examines a simple unified semantics for reasoning with assurance and agreement–with which the power of different classes of solvers and rule engines can be united–and consists of three main parts:

  1. An introduction to complex reasoning problems expressed using logic rules, with recursion, negation, quantification, and aggregation; the key idea of a simple unified semantics, supporting simple expression of different assumptions; and how it unifies different prior semantics.

  2. An overview of the precise rule language; the formal semantics, called Founded Semantics and Constraint Semantics, or Founded + Constraint Semantics (FCS) for short here, supporting efficient and precise inference over aggregation even with approximation; and the properties of the semantics.
  3. An exploration of a wide range of challenging examples, including the well-known problem of company control and extended win-not-win games. FCS is simple and matches the desired results in all cases.
Additionally, we compare 10 different classes of solvers and rule engines and discuss the different semantics they compute and how their power can be united. Such combined power for problem solving and question answering with assurance and agreement is an essential complement to LLMs.

Y. Annie Liu is Professor of Computer Science at Stony Brook University. Her primary research is in languages and algorithms, especially on systematic methods for design and optimization. The methods are centered around incrementalization—the discrete counterpart of differentiation in calculus. Besides research and service, she also enjoys teaching. She has taught in a wide range of Computer Science areas, and presented over 100 conference and invited talks worldwide. She received her BS from Peking University, MEng from Tsinghua University, and PhD from Cornell University, all in Computer Science.

Annie Liu’s Design and Analysis Research Laboratory has projects in modeling and specification, analysis and verification, design and optimization, code generation, and testing. These projects are for optimizing compilers, interactive environments, real-time and embedded systems, database systems, semantic Web, distributed systems, big data analysis, security, and more. Her awards include a State University of New York Chancellor’s Award for Excellence in Scholarship and Creative Activities.

This program is tentative and subject to change.

Mon 20 Jan

Displayed time zone: Mountain Time (US & Canada) change