T. Altenkirch, . Mcbride, . Conor, . Swierstra, and . Wouter, Observational equality, now! Pages 57?68 of: Proceedings of the ACM workshop on programming languages meets program verification, 2007.

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, . Tanter, and . Eric, A theory of gradual effect systems. Pages 283?295 of: Proceedings of the 19th acm sigplan conference on functional programming, 2014.

B. Schwerter, . Felipe, R. Garcia, . Tanter, and . Eric, Gradual type-and-effect systems, Journal of functional programming, vol.26, issue.19, pp.1-1969, 2016.

A. Bauer, . Gross, . Jason, P. Lumsdaine, . Lefanu et al., The HoTT library: a formalization of homotopy type theory in Coq, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, 2017.
DOI : 10.1017/S0960129514000577
URL : https://hal.archives-ouvertes.fr/hal-01421212

S. Boulier, . Pédrot, . Pierre-marie, and N. Tabareau, The next 700 syntactical models of type theory, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, 2017.
DOI : 10.1109/LICS.1989.39193
URL : https://hal.archives-ouvertes.fr/hal-01445835

E. Brady, . Mcbride, . Conor, and J. Mckinna, Inductive Families Need Not Store Their Indices, Chap. Inductive Families Need Not Store Their Indices, pp.115-129, 2004.
DOI : 10.1007/978-3-540-24849-1_8
URL : http://www.cs.st-andrews.ac.uk/~eb/writings/indfamilies.ps

A. Chlipala, Certified programming with dependent types, 2013.

P. Clairambault, Isomorphisms of types in the presence of higher-order references (extended version) Logical methods in computer science, 2012.

J. Cockx, D. Devriese, and F. Piessens, Abstract, Journal of Functional Programming, vol.16, p.16, 2016.
DOI : 10.1017/S095679681300018X

C. Cohen, . Dénès, . Maxime, and A. Mörtberg, Refinements for free! Pages 147?162 of, Proceedings of the 3rd international conference on certified programs and proofs, 2013.

R. Cosmo and . Di, A short survey of isomorphisms of types, Mathematical structures in computer science, pp.825-838, 2005.
DOI : 10.1017/S0960129505004871

P. Dagand, . Evariste, and C. Mcbride, Transporting functions across ornaments, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00922581

. Dagand, . Pierre-evariste, N. Tabareau, and E. Tanter, Partial type equivalences for verified dependent interoperability, Pages 298?310 of: Proceedings of the 21st acm sigplan conference on functional programming, 2016.
DOI : 10.1145/3022670.2951933
URL : https://hal.archives-ouvertes.fr/hal-01328012

B. Delaware, . Pit-claudel, . Clément, J. Gross, and A. Chlipala, Fiat: Deductive synthesis of abstract data types in a proof assistant, Pages 689?700 of: Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2015.

T. Disney and C. Flanagan, Gradual information flow typing. International workshop on scripts to programs, 2011.

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

R. Findler, . Bruce, and M. Felleisen, Contracts for higher-order functions. Pages 48?59 of: Proceedings of the 7th acm sigplan conference on functional programming, 2002.
DOI : 10.1145/583852.581484
URL : http://people.cs.uchicago.edu/~robby/publications/papers/ho-contracts-icfp2002.pdf

R. Garcia, C. , A. M. Tanter, and . Eric, Abstracting gradual typing. Pages 429?442 of, Proceedings of the 43rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2016.
DOI : 10.1145/2914770.2837670

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

M. Hofmann and T. Streicher, The groupoid model refutes uniqueness of identity proofs. Pages 208?212 of: Proceedings of the 9th symposium on logic in computer science (lics '94), 1994.

J. M. Hyland, First steps in synthetic domain theory, Pages 131?156 of: Proceedings of the international conference on category theory, 1991.
DOI : 10.1007/BFb0018350

K. Knowles and C. Flanagan, Hybrid type checking Acm transactions on programming languages and systems, 2010.

. Ko, . Hsiang-shang, and J. Gibbons, Relational algebraic ornaments, Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP '13, 2013.
DOI : 10.1145/2502409.2502413
URL : http://www.cs.ox.ac.uk/people/hsiang-shang.ko/algOrn/algOrn.pdf

O. Laurent, Classical isomorphisms of types, Mathematical structures in computer science, pp.969-1004, 2005.
DOI : 10.1017/S0960129505004895
URL : https://hal.archives-ouvertes.fr/hal-00003761

N. Lehmann, . Tanter, and . Eric, Gradual refinement types. Pages 775?788 of, Proceedings of the 44th ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2017.
DOI : 10.1145/3093333.3009856

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

P. Levy and . Blain, Contextual isomorphisms. Pages 400?414 of, Proceedings of the 44th ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2017.
DOI : 10.1145/3093333.3009898

J. Matthews, R. Findler, and . Bruce, Operational semantics for multi-language programs. Pages 3?10 of, Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2007.
DOI : 10.1145/1190216.1190220
URL : http://people.cs.uchicago.edu/~robby/pubs/papers/popl2007-mf-bw.pdf

C. Mcbride, Elimination with a motive. Pages 197?216 of: International workshop on types for proofs and programs, 2000.

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

J. Mckinna, Why dependent types matter Page 1 of, Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2006.

. Mishra-linger, . Nathan, and T. Sheard, Erasure and polymorphism in pure type systems. Pages 350?364 of: 11th international conference on foundations of software science and computational structures (fossacs), Lecture Notes in Computer Science, vol.4962, 2008.
DOI : 10.1007/978-3-540-78499-9_25
URL : http://web.cecs.pdx.edu/~sheard/papers/FossacsErasure08.pdf

. Osera, . Peter-michael, . Sjöberg, . Vilhelm, and S. Zdancewic, Dependent interoperability. Pages 3?14 of: Proceedings of the 6th workshop on programming languages meets program verification, 2012.

. Ou, . Xinming, . Tan, . Gang, . Mandelbaum et al., Dynamic typing with dependent types. Pages 437?450 of, Proceedings of the ifip international conference on theoretical computer science, 2004.
DOI : 10.1007/1-4020-8141-3_34
URL : http://cis.ksu.edu/~xou/publications/tcs04.pdf

P. Rondon, . Maxim, M. Kawaguchi, and R. Jhala, Liquid types. Pages 159?169 of, Proceedings of the ACM SIGPLAN conference on programming language design and implementation, 2008.
DOI : 10.1145/1379022.1375602

. Sekiyama, . Taro, Y. Nishida, and A. Igarashi, Manifest contracts for datatypes. Pages 195?207 of, Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2015.
DOI : 10.1145/2676726.2676996

J. Siek, . Taha, and . Walid, Gradual typing for functional languages, Pages 81?92 of: Proceedings of the scheme and functional programming workshop, 2006.

J. G. Siek, M. M. Vitousek, . Cimini, . Matteo, J. Boyland et al., Refined criteria for gradual typing. Pages 274?293 of: 1st summit on advances in programming languages, 2015.

M. Sozeau, Equations: A dependent pattern-matching compiler. Pages 419?434 of, Proceedings of the 1st international conference on interactive theorem proving, 2010.
DOI : 10.1007/978-3-642-14052-5_29
URL : https://hal.archives-ouvertes.fr/inria-00628862

M. Sozeau and N. Oury, First-Class Type Classes, Pages 278?293 of: Proceedings of the 21st international conference on theorem proving in higher-order logics, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

. Swierstra, . Wouter, and J. Alpuim, From proposition to program -embedding the refinement calculus in Coq, Pages 29?44 of: Proceedings of the 13th international symposium on functional and logic programming, 2016.

´. Tanter, . Eric, and N. Tabareau, Gradual certified programming in Coq, Proceedings of the 11th ACM dynamic languages symposium, 2015.
DOI : 10.1145/2936313.2816710
URL : https://hal.archives-ouvertes.fr/hal-01238774

P. Thiemann and L. Fennell, Gradual typing for annotated type systems. Pages 47?66 of, Proceedings of the 23rd european symposium on programming languages and systems, 2014.
DOI : 10.1007/978-3-642-54833-8_4

M. Toro, . Tanter, and . Eric, Customizable gradual polymorphic effects for Scala. Pages 935?953 of, Proceedings of the 30th ACM SIGPLAN conference on object-oriented programming systems, languages and applications, 2015.
DOI : 10.1145/2858965.2814315

. The, Homotopy type theory: Univalent foundations of mathematics. Institute for Advanced Study, 2013.

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, 1989.
DOI : 10.1145/75277.75283

T. Williams, P. Dagand, . Evariste, . Rémy, and . Didier, Ornaments in practice. Pages 15?24 of: Magalhães, Proceedings of the 10th ACM SIGPLAN workshop on generic programming, 2014.
DOI : 10.1145/2633628.2633631
URL : https://hal.archives-ouvertes.fr/hal-01081547

H. Xi and F. Pfenning, Eliminating array bound checking through dependent types, Pages 249?257 of: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (pldi '98, 1998.
DOI : 10.1145/277652.277732
URL : http://www.lb.cs.cmu.edu/Groups/fox/people/fp/papers/pldi98dml.ps.gz

T. Zimmermann and H. Herbelin, Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01152588