Logical Predicates in Higher-Order Mathematical Operational Semantics
Goncharov S, Santamaria A, Schröder L, Tsampas S, Urbat H (2024)
Publication Type: Conference contribution
Publication year: 2024
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 14575 LNCS
Pages Range: 47-69
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Luxembourg City, LUX
ISBN: 9783031572302
DOI: 10.1007/978-3-031-57231-9_3
Abstract
We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We start with the observation that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a view to enabling inductive reasoning, and identify sufficient conditions on the overall setup in which locally maximal logical refinements canonically exist. Finally, we develop induction-up-to techniques that simplify inductive proofs via logical predicates on systems encoded as (certain classes of) higher-order GSOS laws by identifying and abstracting away from their boiler-plate part.
Involved external institutions
United Kingdom (GB)How to cite
APA:
Goncharov, S., Santamaria, A., Schröder, L., Tsampas, S., & Urbat, H. (2024). Logical Predicates in Higher-Order Mathematical Operational Semantics. In Naoki Kobayashi, James Worrell (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 47-69). Luxembourg City, LUX: Springer Science and Business Media Deutschland GmbH.
MLA:
Goncharov, Sergey, et al. "Logical Predicates in Higher-Order Mathematical Operational Semantics." Proceedings of the 27th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2024 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, LUX Ed. Naoki Kobayashi, James Worrell, Springer Science and Business Media Deutschland GmbH, 2024. 47-69.
BibTeX: Download