6 citations · 14 across the 5 of their papers we have counts for
7 papers
Compact Quantitative Equational Theories as Monad Restrictions
Matteo Mio, Colin Riba
Proofs in quantitative algebra are, generally, infinite objects due to the presence of infinitary rules in the deductive apparatus. A quantitative equational theory is called compa…
Finitely accessible arboreal adjunctions and Hintikka formulae
Luca Reggio, Colin Riba
Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically…
A Functional (Monadic) Second-Order Theory of Infinite Trees
Anupam Das, Colin Riba
This paper presents a complete axiomatization of Monadic Second-Order Logic (MSO) over infinite trees. MSO on infinite trees is a rich system, and its decidability ("Rabin's Tree T…
A Curry-Howard Approach to Church's Synthesis
Cécilia Pradic, Colin Riba
Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Or…
On the confluence of lambda-calculus with conditional rewriting
Frédéric Blanqui, Claude Kirchner, Colin Riba
The confluence of untyped λ-calculus with unconditional rewriting is now well un- derstood. In this paper, we investigate the confluence of λ-calculus with conditional rewriting an…
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems
Frédéric Blanqui, Colin Riba
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size…
On the confluence of lambda-calculus with conditional rewriting
Frédéric Blanqui, Claude Kirchner, Colin Riba
The confluence of untyped lambda-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of lambda-calcul…