2 papers
cs.LO2025
A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations
Patrick Baillot, Ugo Dal Lago, Cynthia Kop +1
The class of type-two basic feasible functionals () is the analogue of (polynomial time functions) for type-2 functionals, that is, functionals that c…
cs.LO2025
Verifying Procedural Programs via Constrained Rewriting Induction
Carsten Fuhs, Cynthia Kop, Naoki Nishida
This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend tra…