Politeness for the Theory of Algebraic Datatypes

Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories

Cyclic data structures, such as cyclic lists, in functional programming are tricky to handle because of their cyclicity. This paper presents an investigation of categorical, algebraic, and computational foundations of cyclic datatypes. Our framework of cyclic datatypes is based on second-order algebraic theories of Fiore et al., which give a uniform setting for syntax, types, and computation rules for describing and reasoning about cyclic datatypes. We extract the "fold" computation rules from the categorical semantics based on iteration categories of Bloom and Esik. Thereby, the rules are cor…

The Extended Theory of Trees and Algebraic (Co)datatypes

The first-order theory of finite and infinite trees has been studied since the eighties, especially by the logic programming community. Following Djelloul, Dao and Frühwirth, we consider an extension of this theory with an additional predicate for finiteness of trees, which is useful for expressing properties about (not just datatypes but also) codatatypes. Based on their work, we present a simplification procedure that determines whether any given (not necessarily closed) formula is satisfiable, returning a simplified formula which enables one to read off all possible models. Our extension ma…

一种面向代数数据类型的急切可满足性模理论求解器

An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes

针对现有SMT求解器处理代数数据类型（ADTs）时因惰性方法导致扩展性差的问题，提出一种急切方法，将ADT查询归约为未解释函数（UF）理论，并证明了该方法的可靠性、完备性及优于现有方法的性能。

General Interpolation and Strong Amalgamation for Contiguous Arrays

Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the datatype theory of contiguous arrays with maxdiff, where arrays are completely defined in their allocation memory and for which maxdiff returns the max index where they differ. This theory is strictly more expressive than the array theories previously studied. By showing via an algebraic analysis that its models strongly amalgamate, we prove that this theory admits quantifier-free interpolants and, notably, that interpo…

使用表与关系理论验证SQL查询

Verifying SQL Queries using Theories of Tables and Relations

本文提出SMT理论的一阶和二阶扩展，用于表示和分析含连接、投影、选择操作的SQL查询，支持包与集合语义及空值推理，并在cvc5中实现求解器，基于公开基准进行了评估。