1: \begin{thebibliography}{10}
2:
3: \bibitem{Alt-Reus}
4: Thorsten Altenkirch and Bernhard Reus.
5: \newblock Monadic presentations of lambda terms using generalized inductive
6: types.
7: \newblock In {\em {CSL}}, pages 453--468, 1999.
8:
9: \bibitem{BPfold}
10: Richard Bird and Ross Paterson.
11: \newblock Generalised folds for nested datatypes.
12: \newblock {\em Formal Aspects of Computing}, 11(2):200--222, 1999.
13:
14: \bibitem{BPdebruijn}
15: Richard~S. Bird and Ross Paterson.
16: \newblock De {B}ruijn notation as a nested datatype.
17: \newblock {\em Journal of Functional Programming}, 9(1):77--91, 1999.
18:
19: \bibitem{MR2140994}
20: Michael Ching.
21: \newblock Bar constructions for topological operads and the {G}oodwillie
22: derivatives of the identity.
23: \newblock {\em Geom. Topol.}, 9:833--933 (electronic), 2005.
24:
25: \bibitem{Coq}
26: The {Coq Proof Assistant}.
27: \newblock http://coq.inria.fr.
28:
29: \bibitem{FPT}
30: Marcelo Fiore, Gordon Plotkin, and Daniele Turi.
31: \newblock Abstract syntax and variable binding (extended abstract).
32: \newblock In {\em 14th Symposium on Logic in Computer Science (Trento, 1999)},
33: pages 193--202. IEEE Computer Soc., Los Alamitos, CA, 1999.
34:
35: \bibitem{Fiore06}
36: Marcelo~P. Fiore.
37: \newblock On the structure of substitution.
38: \newblock Invited address for the 22nd Mathematical Foundations of Programming
39: Semantics Conf. (MFPS XXII), 2006.
40: \newblock DISI, University of Genova (Italy).
41:
42: \bibitem{FT}
43: Marcelo~P. Fiore and Daniele Turi.
44: \newblock Semantics of name and value passing.
45: \newblock In {\em Logic in Computer Science}, pages 93--104, 2001.
46:
47: \bibitem{MR2066499}
48: Benoit Fresse.
49: \newblock Koszul duality of operads and homology of partition posets.
50: \newblock In {\em Homotopy theory: relations with algebraic geometry, group
51: cohomology, and algebraic $K$-theory}, volume 346 of {\em Contemp. Math.},
52: pages 115--215. Amer. Math. Soc., Providence, RI, 2004.
53:
54: \bibitem{PG}
55: Murdoch Gabbay and Andrew Pitts.
56: \newblock A new approach to abstract syntax involving binders.
57: \newblock In {\em 14th Symposium on Logic in Computer Science (Trento, 1999)},
58: pages 214--224. IEEE Computer Soc., Los Alamitos, CA, 1999.
59:
60: \bibitem{GU03}
61: Neil Ghani and Tarmo Uustalu.
62: \newblock Explicit substitutions and higher-order syntax.
63: \newblock In {\em MERLIN '03: Proceedings of the 2003 ACM SIGPLAN workshop on
64: Mechanized reasoning about languages with variable binding}, pages 1--7, New
65: York, NY, USA, 2003. ACM Press.
66:
67: \bibitem{Algebraicity}
68: Andr\'e Hirschowitz and Marco Maggesi.
69: \newblock The algebraicity of the lambda-calculus.
70: \newblock arXiv:math/0607427v1, 2007.
71:
72: \bibitem{H}
73: Martin Hofmann.
74: \newblock Semantical analysis of higher-order abstract syntax.
75: \newblock In {\em 14th Symposium on Logic in Computer Science (Trento, 1999)},
76: pages 204--213. IEEE Computer Soc., Los Alamitos, CA, 1999.
77:
78: \bibitem{arXiv:math/0607427v1}
79: Muriel Livernet.
80: \newblock From left modules to algebras over an operad: application to
81: combinatorial {H}opf algebras.
82: \newblock arXiv:math/0607427v1, 2006.
83:
84: \bibitem{maclane}
85: Saunders Mac~Lane.
86: \newblock {\em Categories for the working mathematician}, volume~5 of {\em
87: Graduate Texts in Mathematics}.
88: \newblock Springer-Verlag, New York, second edition, 1998.
89:
90: \bibitem{arXiv:hep-th/9411208v1}
91: Martin Markl.
92: \newblock Models for operads.
93: \newblock arXiv:hep-th/9411208v1, 1994.
94:
95: \bibitem{arXiv:hep-th/9608067v1}
96: Martin Markl.
97: \newblock A compactification of the real configuration space as an operadic
98: completion.
99: \newblock arXiv:hep-th/9608067v1, 1996.
100:
101: \bibitem{MU03}
102: Ralph Matthes and Tarmo Uustalu.
103: \newblock Substitution in non-wellfounded syntax with variable binding.
104: \newblock {\em Theor. Comput. Sci.}, 327(1-2):155--174, 2004.
105:
106: \bibitem{smirnov86}
107: V.~A. Smirnov.
108: \newblock Homotopy theory of coalgebras.
109: \newblock {\em Math. USSR Izv,}, 27:575--592, 1986.
110:
111: \bibitem{Power-Tanaka-unified}
112: Miki Tanaka and John Power.
113: \newblock A unified category-theoretic formulation of typed binding signatures.
114: \newblock In {\em MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on
115: Mechanized reasoning about languages with variable binding}, pages 13--24,
116: New York, NY, USA, 2005. ACM Press.
117:
118: \bibitem{Power-Tanaka-pseudo}
119: Miki Tanaka and John Power.
120: \newblock Pseudo-distributive laws and axiomatics for variable binding.
121: \newblock {\em Higher Order Symbol. Comput.}, 19(2-3):305--337, 2006.
122:
123: \bibitem{JZ}
124: Julianna Zsid\'o.
125: \newblock Le lambda calcul vu comme monade initiale.
126: \newblock Master's thesis, Universit\'e de Nice -- Laboratoire
127: J.~A.~Dieudonn\'e, 2005/06.
128: \newblock M\'emoire de Recherche -- master 2.
129:
130: \end{thebibliography}
131: