Sciweavers

Share
ENTCS
2008

Functorial Coalgebraic Logic: The Case of Many-sorted Varieties

8 years 10 months ago
Functorial Coalgebraic Logic: The Case of Many-sorted Varieties
Following earlier work, a modal logic for T-coalgebras is a functor L on a suitable variety. Syntax and proof system of the logic are given by presentations of the functor. This paper makes two contributions. First, a previous result characterizing those functors that have presentations is generalized from endofunctors on one-sorted varieties to functors between many-sorted varieties. This yields an equational logic for the semantics of higher-order abstract syntax. As another application, we show how the move to functors between many-sorted varieties allows to modularly combine syntax and proof systems of different logics. Second, we show how to associate to any set-functor T a complete (finitary) logic L consisting of modal operators and Boolean connectives.
Alexander Kurz, Daniela Petrisan
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Alexander Kurz, Daniela Petrisan
Comments (0)
books