P. Aczel, J. Adámek, and J. Velebil, A Coalgebraic View of Infinite Trees and Iteration, Electronic Notes in Theoretical Computer Science, vol.44, issue.1, pp.1-26, 2001.
DOI : 10.1016/S1571-0661(04)80900-9

A. Abel, Type-based termination: a polymorphic lambda-calculus with sized higher-order types, 2007.

E. Brian, A. Aydemir, B. C. Charguéraud, R. Pierce, S. Pollack et al., Engineering formal metatheory, POPL, pp.3-151328443, 1145.

B. Ahrens, P. Capriotti, and R. Spadotti, Non-wellfounded trees in homotopy type theory, TLCA, pp.17-3017

N. Agh-+-15-]-thorsten-altenkirch, P. Ghani, C. Hancock, P. Mcbride, and . Morris, Indexed containers, Journal of Functional Programming

B. Ahrens, Initiality for Typed Syntax and Semantics, Journal of Formalized Reasoning, vol.8, issue.2, pp.1-1554712
DOI : 10.1007/978-3-642-32621-9_10
URL : https://hal.archives-ouvertes.fr/hal-01329607

R. Atkey and C. Mcbride, Productive coprogramming with guarded recursion, ICFP, pp.197-208

T. Altenkirch and B. Reus, Monadic Presentations of Lambda Terms Using Generalized Inductive Types, CSL, pp.453-468, 1999.
DOI : 10.1007/3-540-48168-0_32

B. Ahrens and R. Spadotti, Terminal semantics for codata types in intensional Martin-Löf type theory, TYPES, volume 39 of LIPIcs, pp.1-26

G. Barthe and T. Coquand, An Introduction to Dependent Type Theory, APPSEM, pp.1-41, 2000.
DOI : 10.1007/3-540-45699-6_1

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Journal of Functional Programming, vol.13, issue.02, pp.261-293, 1017.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-01124972

M. Brandt and F. Henglein, Coinductive axiomatization of recursive type equality and subtyping, TLCA, pp.63-81, 1997.
DOI : 10.1007/3-540-62688-3_29

T. Braibant, J. Jourdan, and D. Monniaux, Implementing Hash-Consed Structures in Coq, ITP, pp.477-483978, 1007.
DOI : 10.1007/978-3-642-39634-2_36
URL : https://hal.archives-ouvertes.fr/hal-00816672

J. A. Bergstra and J. W. Klop, Process theory based on bisimulation semantics, Lecture Notes in Computer Science, vol.354, issue.10, pp.50-122, 1007.
DOI : 10.1007/BFb0013021

L. Stephen and . Bloom, All solutions of a system of recursion equations in infinite trees and other contraction theories, Journal of Computer and System Sciences, vol.2783, issue.2, pp.225-255, 1983.

J. Christian-blanchette, A. Popescu, and D. Traytel, Foundational extensible corecursion: a proof assistant perspective, ICFP, pp.192-204

A. Janusz and . Brzozowski, Canonical regular expressions and minimal state graphs for definite events, Mathematical theory of Automata, vol.12, issue.6, pp.529-561, 1962.

H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard et al., Tree automata techniques and applications, Dominique Devriese, and Frank Piessens. Pattern matching without K. In ICFP, pp.257-268, 1145.

T. Coquand and G. Huet, The calculus of constructions Information and Computation, pp.95-1200890, 1016.

A. Chlipala, Certified Programming with Dependent Types?A Pragmatic Introduction to the Coq Proof Assistant, 2013.

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

C. C??rsteac??rstea, C. Kupke, and D. Pattinson, EXPTIME tableaux for the coalgebraic µ-calculus, Logical Methods in Computer Science, vol.7, issue.333, pp.10-2168, 2011.

C. Cohen, Pragmatic Quotient Types in Coq, ITP, pp.213-228
DOI : 10.1007/978-3-642-39634-2_17

T. Coquand, Infinite objects in type theory, TYPES, pp.62-78, 1993.
DOI : 10.1007/3-540-58085-9_72

T. Coquand and C. Paulin, Inductively defined types, Conference on Computer Logic, pp.50-66
DOI : 10.1007/3-540-52335-9_47

N. Anders-danielsson and T. Altenkirch, Subtyping, Declaratively, PAR, pp.100-118, 2010.
DOI : 10.1007/978-3-642-13321-3_8

N. Govert-de-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indagationes Mathematicae (Proceedings), pp.381-392, 1972.

N. Anders-danielsson and U. Norell, Parsing Mixfix Operators, IFL, pp.80-99, 2008.
DOI : 10.1007/3-540-15975-4_33

A. Brian, H. A. Davey, and . Priestley, Introduction to Lattices and Order, 2002.

J. Endrullis, D. Hendriks, and M. Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, ITP, pp.354-369978, 1007.
DOI : 10.1007/978-3-642-39634-2_26

J. Engelfriet, Top-down tree transducers with regular look-ahead, Mathematical Systems Theory, vol.4, issue.1, pp.289-303, 1007.
DOI : 10.1007/BF01683280

D. Firsov and T. Uustalu, Dependently typed programming with finite sets, Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP 2015, pp.33-44
DOI : 10.1007/978-3-642-04652-0_5

Z. Fülöp and H. Vogler, Syntax-Directed Semantics. Formal Models Based on Tree Transducers. Monographs in Theoretical Computer Science, pp.978-981, 1007.

N. Ghani, M. Hamana, T. Uustalu, and V. Vene, Representing cyclic structures as nested datatypes, Proceedings of 7th Trends in Functional Programming, pp.173-188, 2006.

E. Giménez, A Calculus of Infinite Constructions and its applications to the verification of communicating systems, 1996.

S. Ginali, Regular trees and the free iterative theory, Journal of Computer and System Sciences, vol.18, issue.3, pp.228-242, 1979.
DOI : 10.1016/0022-0000(79)90032-1

J. Girard, Interprétation fonctionnelle etéliminationetélimination des coupures de l'arithmétique d'ordre supérieur, 1972.

P. Genevès, N. Laya¨?dalaya¨?da, A. Schmitt, and N. Gesbert, Efficiently Deciding ??-Calculus with Converse over Finite Trees, ACM Transactions on Computational Logic, vol.16, issue.2, p.16, 2015.
DOI : 10.1145/1375581.1375624

H. Goguen, C. Mcbride, and J. Mckinna, Eliminating Dependent Pattern Matching, Lecture Notes in Computer Science, vol.4060, issue.10, pp.521-540, 1007.
DOI : 10.1007/11780274_27

D. Gustafsson and N. Pouillard, Foldable containers and dependent types, p.2015

M. Hedberg, A coherence theorem for martin-löf's type theory Communicating sequential processes, Journal of Functional Programming Communications of the ACM, vol.8359576, issue.218, pp.413-436666, 1145.

J. E. Hopcroft, An n log n algorithm for minimizing states in a finite automaton CoCaml: Programming with coinductive types, p.30798, 1813.

D. Kozen, Results on the Propositional ??-Calculus, DAIMI Report Series, vol.11, issue.146, pp.333-3540304, 1016.
DOI : 10.7146/dpb.v11i146.7420

N. Li, Quotient types in type theory, 2015.

R. Daniel, M. Licata, and . Shulman, Calculating the fundamental group of the circle in homotopy type theory, LICS, pp.223-232

S. Maneth, Equivalence Problems for Tree Transducers: A Brief Survey, AFL, pp.74-93
DOI : 10.4204/EPTCS.151.5

P. Martin-löf, An intuitionistic theory of types: Predicative part. Studies in Logic and the Foundations of, Mathematics, vol.80, issue.08, pp.73-118, 1975.

P. Martin-löf and G. Sambin, Intuitionistic type theory Studies in proof theory, 1984.

S. Milius and T. Wißmann, Finitary corecursion for the infinitary lambda calculus, CALCO Schloss Dagstuhl?Leibniz- Zentrum für Informatik, pp.336-351

E. Nelson, Iterative algebras, Theoretical Computer Science, vol.25, issue.1, pp.67-940304, 1016.
DOI : 10.1016/0304-3975(83)90014-2

U. Norell, Towards a practical programming language based on dependent type theory, 2007.

E. Parmann, Investigating streamless sets, TYPES, volume 39 of LIPIcs, pp.187-201187

C. Lawrence and . Paulson, Constructing recursion operators in intuitionistic type theory, Journal of Symbolic Computation, vol.2, issue.486, pp.325-355, 1986.

C. Paulin-mohring, Extraction de programmes dans le Calcul des Constructions, 1989.
URL : https://hal.archives-ouvertes.fr/tel-00431825

F. Pfenning and C. Elliott, Higher-order abstract syntax, PLDI, pp.199-20854010, 1145.

C. Picard, Représentation coinductive des graphes, 2012.

A. M. Pitts, Nominal Logic: A First Order Theory of Names and Binding, TACS, pp.219-242, 2001.
DOI : 10.1007/3-540-45500-0_11

C. John and . Reynolds, Towards a theory of type structure, Symposium on Programming, pp.408-423, 1974.

C. William and . Rounds, Trees, transducers and transformations, 1968.

C. William and . Rounds, Mappings and grammars on trees, Mathematical Systems Theory, vol.4, issue.3 10, pp.257-287, 1007.

J. J. Rutten, Universal coalgebra: a theory of systems, Theoretical Computer Science, vol.249, issue.1, pp.3-80, 2000.
DOI : 10.1016/S0304-3975(00)00056-6

S. Sa¨?bisa¨?bi, Typing algorithm in type theory with inheritance, POPL, pp.292-301, 1145.

A. Spiwack and T. Coquand, Constructively Finite? In Contribuciones científicas en honor de Mirian Andrés Gómez, pp.217-230, 2010.

H. Seidl, Deciding Equivalence of Finite Tree Automata, SIAM Journal on Computing, vol.19, issue.3, pp.424-437, 1990.
DOI : 10.1137/0219027

H. Seidl, Equivalence of finite-valued tree transducers is decidable, Mathematical Systems Theory, vol.4, issue.4, pp.285-346, 1994.
DOI : 10.1016/B978-0-12-115350-2.50014-2

M. Sozeau and N. Oury, First-Class Type Classes, TPHOLs, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

M. Sozeau, A new look at generalized rewriting in type theory, Journal of Formalized Reasoning, vol.2, issue.1, pp.41-62, 1574.
URL : https://hal.archives-ouvertes.fr/inria-00628904

M. Sozeau, Equations: A Dependent Pattern-Matching Compiler, ITP, pp.419-434978, 1007.
DOI : 10.1007/978-3-642-14052-5_29
URL : https://hal.archives-ouvertes.fr/inria-00628862

R. Spadotti, A Mechanized Theory of Regular Trees in Dependent Type Theory, ITP, pp.405-420978, 1007.
DOI : 10.1007/978-3-319-22102-1_27

C. Sprenger, A verified model checker for the modal ??-calculus in Coq, TACAS, pp.167-183, 1007.
DOI : 10.1007/BFb0054171

M. Sozeau and N. Tabareau, Universe Polymorphism in Coq, ITP, pp.499-514
DOI : 10.1007/978-3-319-08970-6_32
URL : https://hal.archives-ouvertes.fr/hal-00974721

G. Slutzki and S. Vágvölgyi, Deterministic top-down tree transducers with iterated look-ahead, Theoretical Computer Science, vol.143, issue.2, pp.285-308, 1995.
DOI : 10.1016/0304-3975(94)00111-U

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-309, 1955.
DOI : 10.2140/pjm.1955.5.285

J. W. Thatcher, Generalized sequential machine maps, Journal of Computer and System Sciences, vol.470, issue.4, pp.339-367, 1970.

M. Tsai and B. Wang, Formalization of CTL* in Calculus of Inductive Constructions, ASIAN, pp.316-330, 2006.
DOI : 10.1145/1108906.1108908

S. Arun-kumar, Institute for Advanced Study Reflecting BDDs in Coq, ASIAN, volume 1961 of Lecture Notes in Computer Science, pp.162-181, 2000.

. Intuitivement, deuxélémentséquivalentsdeuxélémentsdeuxélémentséquivalents dans le setoid peuventêtrepeuventêtre indexés par desélémentsdeséléments différents On parle alors d'un setoid faiblement finiment indexé (WFI) Nous avons prouvé que les setoidsénumérablessetoidsénumérables sont faiblement finiment indéxés mais que la réciproque n'est pas vraie constructivement. 1.2. Types et setoids finis