In this seminar, I will introduce Abstract Lipschitz Continuity (ALC), a generalization of the standard Lipschitz continuity notion. While traditional Lipschitz continuity is defined over metric spaces, ALC extends this notion to pre-metric spaces with a partial ordering, ensuring that small variations in the semantic approximations of inputs lead to proportionally bounded differences in the approximations of outputs. A key aspect of ALC is the distinction between two types of approximations: quantitative approximation, captured by pre-metrics, and qualitative (or semantic) approximation, modeled by upper closure operators. I will show how this distinction enables the study of ALC’s relation to other important program (hyper)properties, such as Partial Completeness in abstract interpretation and Abstract Non-Interference in information-flow security. Finally, I will propose a language- and domain-agnostic deductive system for proving the ALC of programs. The goal in designing this deductive system is to track the assumptions required for ALC to ensure a compositional proof.
