T. Altenkirch, C. Mcbride, and W. Swierstra, Observational equality, now! In PLPV, 2007.

A. Asperti, W. Ricciotti, C. S. Coen, and E. Tassi, A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions, Logical Methods in Computer Science, vol.8, issue.1, 2012.
DOI : 10.2168/LMCS-8(1:18)2012

M. Benke, P. Dybjer, and P. Jansson, Universes for generic programs and proofs in dependent type theory, Nordic Journal of Computing, 2003.

E. Brady, J. Chapman, P. Dagand, A. Gundry, C. Mcbride et al., An Epigram implementation

J. Chapman, P. Dagand, C. Mcbride, and P. Morris, The gentle art of levitation, ICFP, pp.3-14, 2010.

P. Dagand and C. Mcbride, Transporting functions across ornaments, ICFP, pp.103-114, 2012.
DOI : 10.1145/2364527.2364544
URL : https://hal.archives-ouvertes.fr/hal-00922581

E. Giménez, Codifying guarded definitions with recursive schemes, Types for Proofs and Programs, pp.39-59, 1995.
DOI : 10.1007/3-540-60579-7_3

R. Harper and C. Stone, A Type-Theoretic interpretation of standard ML, Proof, Language, and Interaction: essays in honour of Robin Milner, 2000.

Z. Luo, Computation and Reasoning, 1994.

C. Mcbride and J. Mckinna, The view from the left, Journal of Functional Programming, vol.14, issue.1, pp.69-111, 2004.
DOI : 10.1017/S0956796803004829

C. Mcbride, H. Goguen, and J. Mckinna, A Few Constructions on Constructors, Types for Proofs and Programs, pp.186-200, 2004.
DOI : 10.1007/11617990_12

B. C. Pierce and D. N. Turner, Local type inference, POPL, 1998.
DOI : 10.1145/345099.345100