A. Aiken and B. R. Murphy, Implementing Regular Tree Expressions, FPLCA 1991, pp.427-447, 1991.

A. Salim-al-sibahi, The Formal Semantics of Rascal Light, 2017.

A. Salim-al-sibahi, A. S. Dimovski, and A. Wasowski, Symbolic execution of high-level transformations, SLE 2016. 207-220, 2016.

A. Salim-al-sibahi, T. P. Jensen, A. S. Dimovski, and A. W?sowski, Verification of High-Level Transformations with Inductive Refinement Types, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01898058

A. Albarghouthi, J. Berdine, B. Cook, and Z. Kincaid, Spatial Interpolants, ESOP 2015. 634-660, 2015.

T. Oana-fabiana-andreescu, S. Jensen, and . Lescuyer, Dependency Analysis of Functional Specifications with Algebraic Data Structures, ICFEM 2015. 116-133, 2015.

B. Basten, J. Van-den-bos, M. Hills, P. Klint, A. Lankamp et al., Modular language implementation in Rascal-Experience, Report. Sci. Comput. Program, vol.114, pp.7-19, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01261480

M. Benke, P. Dybjer, and P. Jansson, Universes for Generic Programs and Proofs in Dependent Type Theory, vol.10, pp.265-289, 2003.

V. Benzaken, G. Castagna, K. Nguyen, and J. Siméon, Static and dynamic semantics of NoSQL languages, POPL 2013, pp.101-114, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00797956

M. Bodin, T. Jensen, and A. Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, CPP 2015. 29-40, 2015.
DOI : 10.1145/2676724.2693174
URL : https://hal.archives-ouvertes.fr/hal-01111588

A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data, VMCAI 2012. 1-22, 2012.
DOI : 10.1007/978-3-642-27940-9_1

M. Bravenboer, K. T. Kalleberg, R. Vermaas, and E. Visser, Stratego/XT 0.17. A language and toolset for program transformation, Sci. Comput. Program, vol.72, pp.52-70, 2008.

G. Castagna and K. Nguyen, Typed iterators for XML, ICFP 2008, pp.15-26, 2008.
DOI : 10.1145/1411203.1411210
URL : https://hal.archives-ouvertes.fr/hal-00336119

E. Bor-yuh, X. Chang, and . Rival, Relational Inductive Shape Analysis, POPL 2008, pp.247-260, 2008.

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

R. James and . Cordy, The TXL source transformation language, Sci. Comput. Program, vol.61, issue.3, pp.190-210, 2006.

P. Cousot, Verification by Abstract Interpretation. In Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, pp.243-268, 2003.
DOI : 10.1007/978-3-540-39910-0_11
URL : https://hal.archives-ouvertes.fr/inria-00528611

P. Cousot and R. Cousot, Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation, FPCA 1995. 170-181, 1995.
DOI : 10.1145/224164.224199

P. Cousot and R. Cousot, Modular Static Program Analysis, CC 2002, pp.159-178, 2002.
DOI : 10.1007/3-540-45937-5_13
URL : https://link.springer.com/content/pdf/10.1007%2F3-540-45937-5_13.pdf

J. Sánchez-cuadrado, E. Guerra, and J. Lara, Static Analysis of Model Transformations, IEEE Trans. Software Eng, vol.43, pp.868-897, 2017.

D. Darais, N. Labich, C. Phuc, D. Nguyen, and . Van-horn, Abstracting definitional interpreters (functional pearl), PACMPL, vol.1, pp.1-12, 2017.
DOI : 10.1145/3110256
URL : http://dl.acm.org/ft_gateway.cfm?id=3110256&type=pdf

F. Emanuele-de-angelis, A. Fioravanti, M. Pettorossi, and . Proietti, Program verification via iterated specialization, Sci. Comput. Program, vol.95, pp.149-175, 2014.

N. Dershowitz and Z. Manna, Proving Termination with Multiset Orderings, Commun. ACM, vol.22, pp.465-476, 1979.
DOI : 10.1145/359138.359142
URL : http://www.dtic.mil/get-tr-doc/pdf?AD%3DADA058601%26Location%3DU2%26doc%3DGetTRDoc.pdf

T. S. Freeman and F. Pfenning, Refinement Types for ML, PLDI 1991, pp.268-277, 1991.
DOI : 10.1145/113445.113468

N. Halbwachs and M. Péron, Discovering properties about arrays in simple programs, PLDI 2008, pp.339-348, 2008.
DOI : 10.1145/1379022.1375623
URL : https://hal.archives-ouvertes.fr/hal-00288274

J. Harrison, Handbook of Practical Logic and Automated Reasoning, 2009.
DOI : 10.1017/cbo9780511576430

D. Van-horn and M. Might, Abstracting abstract machines, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, pp.51-62, 2010.

N. D. Jones, C. K. Gomard, and P. Sestoft, Partial evaluation and automatic program generation, 1993.

P. Klint, T. Van-der, J. Storm, and . Vinju, EASY Metaprogramming with Rascal, pp.222-289, 2011.
DOI : 10.1007/978-3-642-18023-1_6
URL : http://www.cwi.nl/~paulk/publications/rascal-gttse-final.pdf

A. P. Lisitsa and A. P. Nemytykh, Finite Countermodel Based Verification for Program Transformation (A Case Study), Proceedings of the Third International Workshop on Verification and Program Transformation, vol.199, pp.15-32, 2015.
DOI : 10.4204/eptcs.199.2
URL : https://arxiv.org/pdf/1512.03859

J. Liu and X. Rival, An array content static analysis based on non-contiguous partitions, Computer Languages, Systems & Structures, vol.47, pp.104-129, 2017.
DOI : 10.1016/j.cl.2016.01.005
URL : https://hal.archives-ouvertes.fr/hal-01399837

N. Mitchell and C. Runciman, Uniform boilerplate and list processing, pp.49-60, 2007.
DOI : 10.1145/1291201.1291208

A. Mycroft, D. Neil, and . Jones, A relational framework for abstract interpretation, Programs as Data Objects, pp.156-171, 1985.
DOI : 10.1007/3-540-16446-4_9

V. Perrelle and N. Halbwachs, An Analysis of Permutations in Arrays, VMCAI 2010, pp.279-294, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00456558

T. Pham and M. W. Whalen, An Improved Unrolling-Based Decision Procedure for Algebraic Data Types, VSTTE 2013, pp.129-148, 2013.
DOI : 10.1007/978-3-642-54108-7_7

A. Reynolds and V. Kuncak, Induction for SMT Solvers, VMCAI 2015. 80-98, 2015.
DOI : 10.1007/978-3-662-46081-8_5

X. Rival and L. Mauborgne, The trace partitioning abstract domain, ACM Trans. Program. Lang. Syst, vol.29, 2007.

X. Rival, A. Toubhans, and B. Chang, Construction of Abstract Domains for Heterogeneous Properties, pp.489-492, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01095977

M. Rosendahl, Abstract Interpretation as a Programming Language, Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, pp.84-104, 2013.

J. M. Rushby, S. Owre, and N. Shankar, Subtypes for Specifications: Predicate Subtyping in PVS, IEEE Trans. Software Eng, vol.24, pp.709-720, 1998.

A. David and . Schmidt, Trace-Based Abstract Interpretation of Operational Semantics, Lisp and Symbolic Computation, vol.10, pp.237-271, 1998.

D. S. Scott, Data Types as Lattices, SIAM J. Comput, vol.5, pp.522-587, 1976.
DOI : 10.1007/bfb0079432

P. Sestoft and N. Hallenberg, Programming language concepts, 2017.
DOI : 10.1007/978-3-319-60789-4

. Anthonym and . Sloane, Lightweight Language Processing in Kiama, Lecture Notes in Computer Science, vol.6491, pp.408-425, 2011.

B. Michael, G. D. Smyth, and . Plotkin, The CategoryTheoretic Solution of Recursive Domain Equations, SIAM J. Comput, vol.11, pp.761-783, 1982.

M. Heine-sørensen, R. Glück, and N. D. Jones, A Positive Supercompiler, J. Funct. Program, vol.6, pp.811-838, 1996.

P. Suter, M. Dotta, and V. Kuncak, Decision procedures for algebraic data types with abstractions, pp.199-210, 2010.
DOI : 10.1145/1707801.1706325
URL : http://lara.epfl.ch/~kuncak/papers/SuterETAL10DecisionProceduresforAlgebraicDataTypesAbstractions.pdf

A. Toubhans, -. Bor, X. Chang, and . Rival, Reduced Product Combination of Abstract Domains for Shapes, VMCAI 2013, pp.375-395, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00760428

N. Vazou, P. Maxim-rondon, and R. Jhala, Abstract Refinement Types, ESOP 2013. 209-228, 2013.
DOI : 10.1007/978-3-642-37036-6_13
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-37036-6_13.pdf

G. Winskel, Information Systems, p.12, 1993.

N. Wirth, Compiler Construction, 1996.

H. Xi and F. Pfenning, Eliminating Array Bound Checking Through Dependent Types, PLDI 1998, pp.249-257, 1998.