A. Isbn-tsort-sset, 1145/nnnnnnn.nnnnnnn Quote Recursively Definition add quoted := Nat.add. Check eq refl : add quoted = PType "Coq.Init.Datatypes 1) :: nil)%list |}) :: nil) (PConstr, tInd (mkInd "Coq.Init.Datatypes.nat" 0)) (tProd (nNamed "m") (tInd (mkInd "Coq.Init.Datatypes.nat" 0)) (tInd (mkInd "Coq.Init.Datatypes

A. Anand and G. Morrisett, Revisiting Parametricity: Inductives and Uniformity of Propositions, CoqPL'18, 2018.

A. Anand, A. Appel, G. Morrisett, Z. Paraskevopoulou, R. Pollack et al., CertiCoq: A verified compiler for Coq, CoqPL, 2017.

B. Barras, Auto-validation d'un système de preuves avec familles inductives, Thèse de doctorat, 1999.

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

Y. Forster and F. Kunze, Verified Extraction from Coq to a Lambda- Calculus, Coq Workshop 2016, 2016.

G. Jaber, G. Lewertowski, P. Pédrot, M. Sozeau, and N. Tabareau, The Definitional Side of the Forcing, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pp.367-376, 2016.
DOI : 10.1007/BFb0014566
URL : https://hal.archives-ouvertes.fr/hal-01319066

G. Michael and M. , Extensible Proof Engineering in Intensional Type Theory, 2014.

P. Pédrot and N. Tabareau, An effectful way to eliminate addiction to dependence, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp.1-12, 2017.
DOI : 10.1109/LICS.2017.8005113