T. Altenkirch and A. Kaposi, Towards a cubical type theory without an interval. Accepted for publication in LIPIcs, 2017.

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://strictlypositive.org/obseqnow.pdf

A. Anand and G. Morrisett, Revisiting parametricity: Inductives and uniformity of propositions. CoRR, abs, 1163.

J. Bacon, The untenability of genera. Logique et Analyse, pp.197-208, 1974.

A. Bauer, J. Gross, P. Lefanu-lumsdaine, M. Shulman, M. Sozeau 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, pp.164-172, 2017.
DOI : 10.1017/S0960129514000577
URL : https://hal.archives-ouvertes.fr/hal-01421212

J. Bernardy, T. Coquand, and G. Moulin, A Presheaf Model of Parametric Type Theory, Electronic Notes in Theoretical Computer Science, vol.319, pp.67-82, 2015.
DOI : 10.1016/j.entcs.2015.12.006

J. Bernardy, P. Jansson, and R. Paterson, Proofs for free, Journal of Functional Programming, vol.83, issue.02, pp.107-152, 2012.
DOI : 10.1007/BFb0037116

S. Boulier, P. Pédrot, 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, pp.182-194, 2017.
DOI : 10.1109/LICS.1989.39193
URL : https://hal.archives-ouvertes.fr/hal-01445835

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom. Accepted for publication in LIPIcs, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01378906

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

N. Gambino and M. Hyland, Wellfounded Trees and Dependent Polynomial Functors, Proceedings of Types for Proofs and Programs, pp.210-225, 2003.
DOI : 10.1007/978-3-540-24849-1_14
URL : http://www.cs.le.ac.uk/people/ngambino/Publications/gambino-hyland.pdf

F. Haftmann, A. Krauss, O. Kun?ar, and T. Nipkow, Data Refinement in Isabelle/HOL, pp.100-115
DOI : 10.1007/978-3-642-39634-2_10
URL : http://www21.in.tum.de/~krauss/papers/data-refinement-itp13.pdf

B. Huffman and O. Kun?ar, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Proceedings of the 3rd International Conference on Certified Programs and Proofs (CPP 2013), pp.131-146, 2013.
DOI : 10.1007/978-3-319-03545-1_9

R. Neelakantan, D. Krishnaswami, and . Dreyer, Internalizing relational parametricity in the extensional calculus of constructions, Proceedings of the Conference for Computer Science Logic, pp.432-451, 2013.

P. Lammich, Automatic Data Refinement, pp.84-99
DOI : 10.1007/978-3-642-39634-2_9

N. Magaud, Changing Data Representation within the Coq System, International Conference on Theorem Proving in Higher Order Logics, 2003.
DOI : 10.1007/10930755_6

N. Magaud and Y. Bertot, Changing Data Structures in Type Theory: A Study of Natural Numbers, International Workshop on Types for Proofs and Programs, pp.181-196, 2000.
DOI : 10.1007/3-540-45842-5_12

P. Martin-löf, An intuitionistic theory of types, 1971.

C. Paulin-mohring, Introduction to the Calculus of Inductive Constructions, All about Proofs, Proofs for All, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01094195

D. Simon-peyton-jones, S. Vytiniotis, G. Weirich, and . Washburn, Simple unification-based type inference for GADTs, Proceedings of the 11th ACM SIGPLAN Conference on Functional Programming, pp.50-61, 2006.

C. John and . Reynolds, Types, abstraction and parametric polymorphism, IFIP Congress, pp.513-523, 1983.

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

P. Wadler, Theorems for free! In Functional Programming Languages and Computer Architecture, pp.347-359, 1989.

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