@inbook {1997,
	title = {Initial Algebras of Terms With Binding and Algebraic Structure},
	booktitle = {Categories and Types in Logic, Language, and Physics - Lecture Notes in Computer Science},
	volume = {8222},
	year = {2014},
	pages = {211-234},
	publisher = {Springer},
	organization = {Springer},
	abstract = {<p>One of the many results which makes Joachim Lambek famous is: an initial algebra of an endofunctor is an isomorphism. This fixed point result is often referred to as {\textquoteleft}{\textquoteleft}Lambek{\textquoteright}s Lemma{\textquoteright}{\textquoteright}. In this paper, we illustrate the power of initiality by exploiting it in categories of algebra-valued presheaves $\EM(T)^{\N}$, for a monad $T$ on $\Sets$.<br />
The use of presheaves to obtain certain calculi of expressions (with variable binding) was introduced by Fiore, Plotkin, and Turi. They used set-valued presheaves, whereas here the presheaves take values in a category $\EM(T)$ of Eilenberg-Moore algebras. This generalisation allows us to develop a theory where more structured calculi can be obtained. The use of algebras means also that we work in a linear context and need a separate operation $\bang$ for replication, for instance to describe strength for an endofunctor on $\EM(T)$. We apply the resulting theory to give systematic descriptions of non-trivial calculi: we introduce non-deterministic and weighted lambda terms and expressions for automata as initial algebras, and we formalise relevant equations diagrammatically.</p>
},
	url = {http://link.springer.com/chapter/10.1007\%2F978-3-642-54789-8_12},
	author = {Alexandra Silva and Bart Jacobs}
}