2025/07/14 by Simon Guilloud, Guilloud, Simon, Viktor Kunčak +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Polynomial and algebraic computation #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2507.10482
openalex publication_date 2025/07/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We propose to use orthologic as the basis for designing type systems supporting intersection, union, and negation types in the presence of subtyping assumptions. We show how to extend orthologic to support monotonic and antimonotonic functions, supporting the use of type constructors in such type systems. We present a proof system for orthologic with function symbols, showing that it admits partial cut elimination. Using these insights, we present an \mathcal O(n2(1+m)) algorithm for deciding the subtyping relation under m assumptions. We also show O(n2) polynomial-time normalization algorithm, allowing simplification of types to their minimal canonical form.