A general account of coinduction up-to (Q523132)

Up-to techniques were introduced in [\textit{R. Milner}, Communication and concurrency. New York etc.: Prentice Hall (1989; Zbl 0683.68008)]. The authors of the paper under review prove the soundness of such techniques in a fibrational setting, building on the work [\textit{C. Hermida} and \textit{B. Jacobs}, Inf. Comput. 145, No. 2, 107--152 (1998; Zbl 0941.18006)]. This allows them to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. For instance, the fact that bisimulations up to context can be safely used in any language specified by GSOS rules can also be proved in the proposed framework by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras [\textit{D. Turi} and \textit{G. D. Plotkin}, ``Towards a mathematical operational semantics'', in: Proceedings of the twelfth annual IEEE symposium on logic in computer science, LICS '97. Los Alamitos: IEEE Computer Society Press. 280--291 (1997)]. In the second part of the paper, the soundness of up-to contextual closure for weak bisimulations of systems is specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Thus, the categorical framework developed in the first part is extended to an ordered setting. This paper is an extended version of [the authors, ``Coinduction up-to in a fibrational setting'', in: Proceedings of the joint meeting of the 23rd EACSL annual conference on computer science logic (CSL) and the 29th annual ACM/IEEE symposium on logic in computer science, CSL-LICS'14. New York, NY: Association for Computing Machinery (ACM). Article No. 20, 9 p. (2014; \url{doi:10.1145/2603088.2603149}); LIPICS -- Leibniz Int. Proc. Inform. 42, 240--253 (2015; Zbl 1371.68187)]. Section 2 contains motivating examples. Coinduction and up-to techniques are introduced in Section 3, before recalling the basic definitions of fibrations (Section 4) and coinductive predicates (Section 5). The main results are developed in Section 6, where up-to techniques in a fibrational setting are obtained. Section 7 is devoted to technical results allowing to import tools from abstract GSOS specifications. At this point, several examples of the developed theory are given at work (Section 8). Then, in Section 9, the difficulties are explained that arise with weak bisimulation, which motivates an extension of proposed framework to an ordered setting (Section 10). In Section 11, the authors come back to abstract GSOS specifications in the ordered setting, before dealing with weak bisimulation in Section 12, and simulation in Section 13. They conclude with directions for future work in Section 14. For the sake of clarity, the authors postponed many proofs to the appendices, whose structure follows that of the main text.