A categorical framework for equational logics is presented, together with axiomatizability results in the style of Birkhoff. The distinctive categorical structures used are inclusion systems, which are an alternative to factorization systems in which factorization is required to be unique rather than unique ‘up to an isomorphism’. In this framework, models are any objects, and equations are special epimorphisms in [Cfr ], while satisfaction is injectivity. A first result says that equations-as-epimorphisms define exactly the quasi-varieties, suggesting that epimorphisms actually represent conditional equations. In fact, it is shown that the projectivity/freeness of the domain of epimorphisms is what makes the difference between unconditional and conditional equations, the first defining the varieties, as expected. An abstract version of the axiom of choice seems to be sufficient for free objects to be projective, in which case the definitional power of equations of projective and free domain, respectively, is the same. Connections with other abstract formulations of equational logics are investigated, together with an organization of our logic as an institution.

We use some results of Trnková to show first that subcoalgebras are always closed under finite intersections. Assuming that the type functor F is bounded, we obtain a concrete representation of the terminal F-coalgebra. We also provide several equivalent characterizations of boundedness.

We present a category of locally convex topological vector spaces that is a model of propositional classical linear logic and is based on the standard concept of Köthe sequence spaces. In this setting, the ‘of course’ connective of linear logic has a quite simple structure of a commutative Hopf algebra. The co-Kleisli category of this linear category is a cartesian closed category of entire mappings. This work provides a simple setting in which typed λ-calculus and differential calculus can be combined; we give a few examples of computations.

We present an axiomatic framework for Girard's Geometry of Interaction based on the notion of linear combinatory algebra. We give a general construction on traced monoidal categories, with certain additional structure, that is sufficient to capture the exponentials of Linear Logic, which produces such algebras (and hence also ordinary combinatory algebras). We illustrate the construction on six standard examples, representing both the ‘particle-style’ as well as the ‘wave-style’ Geometry of Interaction.

We show a method for translating concurrent systems into partially ordered sets in a functorial way. This is done in a way resembling the construction of the fundamental groups in topology. Since the morphisms of concurrent systems have a flavour of the implementability of one system in another, the functor provides a tool for proving certain non-implementability results.