\begin{thebibliography}{99}

% \bibitem{alt-monads}
% Thorsten Altenkirch, James Chapman and Tarmo Uustalu.
% Monads need not be Endofunctors.
% In: Proc. FOSSACS 2010, LNCS ????, pages ???, Springer, 2010.

\bibitem{bwttt}
Michael Barr and Charles Wells. 
Toposes, Triples and Theories.
Springer-Verlag, 1983, or see
\url{http://www.cwru.edu/artsci/math/wells/pub/ttt.html} 

\bibitem{cockett}
Robin Cockett.  Lecture Notes.  
\url{http://pages.cpsc.ucalgary.ca/~robin/class/617/notes.pdf}

% \bibitem{prfs}
% Jeremy Dawson.
% Isabelle proofs: 
% \url{http://users.rsise.anu.edu.au/~jeremy/isabelle/monad/}.

\bibitem{dosen-bsl}
Kosta Došen. Deductive Completeness.
Bull. Symbolic Logic Volume 2, Number 3 (1996), 243--283.
\url{http://www.math.ucla.edu/~asl/bsl/0203/0203-001.ps}

% \bibitem{hinze-monadic}
% Ralf Hinze. Monadic-style backtracking. Technical Report IAI-TR-96-9,
% Institut fur Informatik III, Universitat Bonn, October 1996.

\bibitem{homeier}
Peter Homeier. The HOL-Omega Logic.
% In: S. Berghofer et al (eds.) TPHOLs 2009, LNCS, vol. 5674, pp. 244--259.
In: Proc. TPHOLs 2009, LNCS, vol. 5674, pp. 244--259.
Springer, Heidelberg (2006) 

\bibitem{huet-saibi}
G\'erard P. Huet \& Amokrane Sa\"ibi.
Constructive category theory. 
% In: Gordon Plotkin, Colin Stirling \& Mads Tofte (eds)
In: Plotkin, Stirling, Tofte (eds)
Proof, Language, and Interaction, MIT Press, 2000, 239-276.

\bibitem{jones-composing}
Mark P Jones and Luc Duponcheel. Composing Monads,
Research Report YALEU/DCS/RR-1004, Yale University, December 1993

\bibitem{kkr}
Dexter Kozen, Christoph Kreitz, and Eva Richter.
Automating proofs in category theory.
% In: Proc. 3rd Int. Joint Conf. Automated Reasoning (IJCAR'06),
In: Proc. IJCAR'06,
LNAI, vol. 4130, pp 392-407. Springer, August 2006.

\bibitem{levy-thesis}
Paul Levy.  Call-By-Push-Value. PhD thesis, 
Queen Mary and Westfield College, London, 2001.
\url{http://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf}

\bibitem{lhj} Sheng Liang, Paul Hudak, and Mark P Jones.
Monad Transformers and Modular Interpreters.
In Proc. Principles of Programming Languages (POPL'95), 333--343.

\bibitem{maclane-categories} Saunders MacLane.
Categories for the Working Mathematician.
% Graduate Texts in Mathematics.
Springer, 1971.

\bibitem{manes} Ernest Manes.  Algebraic theories.
Graduate Texts in Mathematics, Springer, 1976.

\bibitem{moggi} Eugenio Moggi.  
Computational lambda-calculus and monads. 
In Proceedings of Logic in Computer Science (LICS'89), 1989.

\bibitem{turi} Daniele Turi.
Category Theory Lecture Notes.
\url{http://www.dcs.ed.ac.uk/home/dt/CT/categories.pdf}.

\bibitem{wadler-essence} Philip Wadler. The Essence of Functional Programming.
In Symposium on Principles of Programming Languages (POPL'92), 1992, 1--14.

% \bibitem{wadler-free}
% Philip Wadler.  Theorems for free!
% In 4'th International Conference on Functional Programming and
% Computer Architecture, ACM Press, 1989, 347--359. 


\end{thebibliography}

