J. Bénabou, Distributors at work. Notes from a course at TU Darmstadt, 2000.

B. Biering, L. Birkedal, and N. Torp-smith, BI-hyperdoctrines, higher-order separation logic, and abstraction, ACM Transactions on Programming Languages and Systems, vol.29, issue.5, p.29, 2007.
DOI : 10.1145/1275497.1275499

L. Birkedal, N. Torp-smith, and H. Yang, Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages, Logical Methods in Computer Science, vol.2, issue.5, 2006.
DOI : 10.2168/LMCS-2(5:1)2006

J. Carette, O. Kiselyov, and C. Shan, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages, Journal of Functional Programming, vol.2, issue.05, p.19, 2009.
DOI : 10.1016/0890-5401(91)90052-4

P. Dagand and C. Mcbride, A Categorical Treatment of Ornaments, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013.
DOI : 10.1109/LICS.2013.60
URL : https://hal.archives-ouvertes.fr/hal-01081545

P. De and G. , Towards Abstract Categorial Grammars, Assoc. for Computational Linguistics, 39th Annual Meeting, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00100529

T. Freeman and F. Pfenning, Refinement Types for ML. PLDI, 1991.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

C. Hermida, Fibrations, Logical Predicates and Indeterminates, DAIMI Report Series, vol.22, issue.462, 1993.
DOI : 10.7146/dpb.v22i462.6935

C. A. Hoare, An Axiomatic Basis for Computer Programming, Communications of the ACM, vol.12, p.10, 1969.

B. Jacobs, Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141, 1999.

S. Katsumata, Relating Computational Effects by ??- Lifting, 2011.
DOI : 10.1016/j.ic.2012.10.014
URL : http://dx.doi.org/10.1016/j.ic.2012.10.014

M. Kelly, Basic concepts in enriched category theory, CUP, 1982.

J. Lambek, The mathematics of sentence structure, American Mathematical Monthly, vol.65, issue.3, 1958.

J. Lambek and P. Scott, Introduction to Higher-order Categorical Logic, CUP, 1986.

F. and W. Lawvere, FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES, Proceedings of the National Academy of Sciences, vol.50, issue.5, 1963.
DOI : 10.1073/pnas.50.5.869

F. and W. Lawvere, Adjointness in Foundations, dialectica, vol.71, issue.3-4, pp.281-296, 1969.
DOI : 10.1073/pnas.50.5.869

W. Lovas, Refinement types for logical frameworks, 2010.

S. Mac and L. , Categories for the Working Mathematician, 1971.

C. Mcbride, Ornamental Algebras, Algebraic Ornaments, JFP, issue.8, 2010.

W. O. Peter, D. J. Hearn, and . Pym, The Logic of Bunched Implications, BSL, vol.5, issue.2, 1999.

W. O. Peter, H. Hearn, and . Yang, A Semantic Basis for Local Reasoning, FOSSACS, 2002.

J. Frank and . Oles, A Category-Theoretic Approach to the Semantics of Programming Languages, 1982.

F. Pfenning, Refinement Types for Logical Frameworks. Workshop on Types for Proofs and Programs, 1993.

F. Pfenning, Church and Curry: Combining Intrinsic and Extrinsic Typing, Studies in Logic, vol.17, pp.303-338, 2008.

C. John and . Reynolds, The Essence of Algol, Algorithmic Languages, pp.345-372, 1981.

C. John and . Reynolds, The Coherence of Languages with Intersection Types, 1991.

C. John and . Reynolds, Theories of Programming Languages, CUP, 1998.

C. John and . Reynolds, The Meaning of Types: from Intrinsic to Extrinsic Semantics, 2000.

C. John and . Reynolds, Separation logic: A Logic for Shared Mutable Data Structures, LICS, 2002.