T. Altenkirch, C. Mcbride, and W. Swierstra, Observational equality, now!, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.57-68, 2007.
DOI : 10.1145/1292597.1292608
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.207.4309

S. Awodey and A. Bauer, Propositions as [Types], Journal of Logic and Computation, vol.14, issue.4, pp.447-471, 2004.
DOI : 10.1093/logcom/14.4.447

F. Bañados, R. Garcia, and . Tanter, A theory of gradual effect systems, Proceedings of the 19th ACM SIGPLAN Conference on Functional Programming, pp.283-295, 2014.

J. Bénabou, Introduction to bicategories, Reports of the Midwest Category Seminar, pp.1-77, 1967.
DOI : 10.1007/BF01451367

E. Brady, C. Mcbride, and J. Mckinna, Inductive Families Need Not Store Their Indices, chapter Inductive Families Need Not Store Their Indices, pp.115-129, 2004.
DOI : 10.1007/978-3-540-24849-1_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.3849

A. Chlipala, Certified Programming with Dependent Types, 2013.

C. Cohen, M. Dénès, and A. Mörtberg, Refinements for Free!, Proceedings of the 3rd International Conference on Certified Programs and Proofs, pp.147-162, 2013.
DOI : 10.1007/978-3-319-03545-1_10
URL : https://hal.archives-ouvertes.fr/hal-01113453

P. Dagand and C. Mcbride, Transporting functions across ornaments, Proceedings of the 17th ACM SIGPLAN Conference on Functional Programming (ICFP 2012), pp.103-114, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00922581

B. Delaware, C. Pit-claudel, J. Gross, and A. Chlipala, Fiat: Deductive synthesis of abstract data types in a proof assistant, Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.689-700, 2015.

T. Disney and C. Flanagan, Gradual information flow typing, International Workshop on Scripts to Programs, 2011.

L. Fennell and P. Thiemann, Gradual Security Typing with References, 2013 IEEE 26th Computer Security Foundations Symposium, pp.224-239, 2013.
DOI : 10.1109/CSF.2013.22

R. B. Findler and M. Felleisen, Contracts for higher-order functions, Proceedings of the 7th ACM SIGPLAN Conference on Functional Programming, pp.48-59, 2002.
DOI : 10.1145/581478.581484
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.4081

R. Garcia, A. M. Clark, and . Tanter, Abstracting gradual typing, Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.429-442, 2016.
DOI : 10.1145/2837614.2837670
URL : http://repositorio.uchile.cl/handle/2250/140079

G. Gonthier and A. Mahbouhi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

J. M. Hyland, First steps in synthetic domain theory, Proceedings of the International Conference on Category Theory, pp.131-156, 1991.
DOI : 10.1016/0022-4049(82)90030-5

K. Knowles and C. Flanagan, Hybrid type checking, ACM Transactions on Programming Languages and Systems, vol.32, issue.2, 2010.
DOI : 10.1145/1667048.1667051

H. Ko and J. Gibbons, Relational algebraic ornaments, Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP '13, pp.37-48, 2013.
DOI : 10.1145/2502409.2502413
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.637.4220

P. Letouzey, Programmation fonctionnelle certifiée ? L'extraction de programmes dans l'assistant Coq, 2004.

J. Matthews and R. B. Findler, Operational semantics for multi-language programs, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.3-10, 2007.
DOI : 10.1145/1498926.1498930
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.4961

C. Mcbride, Ornamental algebras, algebraic ornaments URL https, 2010.

T. Mishra-linger and . Sheard, Erasure and Polymorphism in Pure Type Systems, 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), pp.350-364, 2008.
DOI : 10.1007/978-3-540-78499-9_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.2558

P. Osera, V. Sjöberg, and S. Zdancewic, Dependent interoperability, Proceedings of the sixth workshop on Programming languages meets program verification, PLPV '12, pp.3-14, 2012.
DOI : 10.1145/2103776.2103779

X. Ou, G. Tan, Y. Mandelbaum, and D. Walker, Dynamic Typing with Dependent Types, Proceedings of the IFIP International Conference on Theoretical Computer Science, pp.437-450, 2004.
DOI : 10.1007/1-4020-8141-3_34
URL : http://cis.ksu.edu/~xou/publications/tcs04.pdf

P. M. Rondon, M. Kawaguchi, and R. Jhala, Liquid types, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.159-169, 2008.
DOI : 10.1145/1379022.1375602

T. Sekiyama, Y. Nishida, and A. Igarashi, Manifest contracts for datatypes, Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on 2016, p.28
DOI : 10.1145/2775051.2676996

J. Siek and W. Taha, Gradual typing for functional languages, Proceedings of the Scheme and Functional Programming Workshop, pp.81-92, 2006.

M. Sozeau and N. Oury, First-Class Type Classes, Proceedings of the 21st International Conference on Theorem Proving in Higher-Order Logics, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

W. Swierstra and J. Alpuim, From proposition to program -embedding the refinement calculus in Coq, Proceedings of the 13th International Symposium on Functional and Logic Programming, pp.29-44, 2016.

´. E. Tanter and N. Tabareau, Gradual certified programming in Coq, Proceedings of the 11th ACM Dynamic Languages Symposium (DLS 2015), pp.26-40, 2015.
DOI : 10.1145/2936313.2816710
URL : https://hal.archives-ouvertes.fr/hal-01238774

P. Wadler and S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, pp.60-76, 1989.
DOI : 10.1145/75277.75283

T. Williams, P. Dagand, and D. Rémy, Ornaments in practice, Proceedings of the 10th ACM SIGPLAN workshop on Generic programming, WGP '14, pp.15-24, 2014.
DOI : 10.1145/2633628.2633631
URL : https://hal.archives-ouvertes.fr/hal-01081547