The following summary was generated by AI from the slides.
Re² (by Knoth, Wang, Polikarpova, and Hoffmann) is a type system that unifies liquid types — polymorphic refinement types with predicate-abstraction qualifiers over a decidable logic — and Automatic Amortized Resource Analysis (AARA), enabling a single type to simultaneously carry a functional correctness refinement and a numeric potential annotation. The combined type grammar introduces resource-annotated types where supports addition and size expressions, affine arrow types annotated with pre/post potential, and A-Normal Form expressions evaluated under a resource-aware small-step semantics with an explicit tick primitive. Type-checking reduces to SMT-dischargeable verification conditions, demonstrated on list append, which receives both a refinement tracking output size as and a resource bound of function calls.