L. Libin, Montagu, Jeremy, SLE'20, 2020.

J. Aldrich, R. J. Simmons, and K. Shin, SASyLF, Proceedings of the 2008 international workshop on Functional and declarative programming in education - FDPE '08, pp.31-40, 2008.

D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur et al., Abella: A System for Reasoning about Relational Specifications, Journal of Formalized Reasoning, vol.7, issue.2, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

L. Bettini, A DSL for writing type systems for Xtext languages, Proceedings of the 9th International Conference on Principles and Practice of Programming in Java - PPPJ '11, pp.31-40, 2011.

L. Cardelli, Type Systems, Computer Science Handbook, pp.2327-2358, 2004.

J. Cheney, Toward a general theory of names, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding - MERLIN '05, pp.33-40, 2005.

A. Church, A formulation of the simple theory of types, Journal of Symbolic Logic, vol.5, issue.2, pp.56-68, 1940.

M. Cimini, , 2015.

M. Cimini, Early Experience in Teaching the Basics of Functional Language Design with a Language Type Checker, Lecture Notes in Computer Science, pp.21-37, 2020.

B. Delaware, B. C. D.-s.-oliveira, and T. Schrijvers, Meta-theory à la carte, Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13, pp.207-218, 2013.

S. Efftinge and M. Spönemann,

B. D. Surla, Developing an Eclipse editor for MARC records using Xtext, Software: Practice and Experience, vol.43, issue.11, pp.1377-1392, 2012.

S. Erdweg, T. Rendel, C. Kästner, and K. Ostermann, SugarJ, Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, pp.391-406, 2011.

S. Erdweg, T. Van-der-storm, M. Völter, M. Boersma, R. Bosman et al., The State of the Art in Language Workbenches, Software Language Engineering, vol.8225, pp.197-217, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00923386

H. Huttel, Typed programming languages, Transitions and Trees, vol.1816, pp.185-210

S. Erdweg, T. Van-der-storm, M. Völter, L. Tratt, R. R. Bosman et al., Evaluating and comparing language workbenches, Computer Languages, Systems & Structures, vol.44, pp.24-47, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01261481

M. Felleisen, R. B. Findler, and M. Flatt, Semantics Engineering with PLT Redex, 2009.

M. Fowler, Tadié, Prof. Jean-Yves, (born 7 Sept. 1936), Chevalier de la Légion d?honneur, 2002; Chevalier de l?Ordre National du Mérite, 1974; Officier des Palmes académiques, 1988; Commandeur de l?Ordre des Arts et des Lettres, 2011; Professor of French Literature, Université de Paris-Sorbonne, 1991?2005, now Emeritus; Editor, Gallimard, since 1991, 2007.

S. Grewe, Automating Type Soundness Proofs for Domain-Specific Languages, 2019.

S. Grewe, S. Erdweg, and M. Mezini, Using Vampire in Soundness Proofs of Type Systems, Proceedings of the 1st and 2nd

S. Grewe, S. Erdweg, and M. Mezini, Using Vampire in Soundness Proofs of Type Systems, Vampire Workshops (EPiC Series in Computing, vol.38, pp.33-51

S. Grewe, S. Erdweg, and M. Mezini, Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny, Vampire 2016. Proceedings of the 3rd Vampire Workshop (EPiC Series in Computing, vol.44, pp.33-45

S. Grewe, S. Erdweg, P. Wittmann, and M. Mezini, Type systems for the masses: deriving soundness proofs and efficient checkers, 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!) - Onward! 2015, pp.137-150, 2015.

R. Harper, Practical Foundations for Programming Languages, 2009.

R. Harper and C. Stone, A Type-Theoretic Interpretation of Standard ML, Proof, Language, and Interaction, 2000.

A. Igarashi, B. C. Pierce, and P. Wadler, Featherweight Java, ACM Transactions on Programming Languages and Systems, vol.23, issue.3, pp.396-450, 2001.

C. L. Lennart, E. Kats, and . Visser, The Spoofax Language Workbench: Rules for Declarative Specification of Languages and IDEs, Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, pp.444-463, 2010.

F. Lorenzen and S. Erdweg, Sound type-dependent syntactic language extension, ACM SIGPLAN Notices, vol.51, issue.1, pp.204-216, 2016.

D. Marino and T. Millstein, A generic type-and-effect system, Proceedings of the 4th international workshop on Types in language design and implementation - TLDI '09, pp.39-50, 2008.

D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell, Lem, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming - ICFP '14, pp.175-188, 2014.

P. Neron, A. P. Tolmach, E. Visser, and G. Wachsmuth, A Theory of Name Resolution, Programming Languages and Systems, vol.9032, pp.205-231, 2015.

S. Owens, M. O. Myreen, R. Kumar, and Y. K. Tan, Functional Big-Step Semantics, Programming Languages and Systems, vol.9632, pp.589-615, 2016.

F. Pfenning and C. Schürmann, System Description: Twelf ? A Meta-Logical Framework for Deductive Systems, Automated Deduction ? CADE-16, pp.202-206, 1999.

C. Benjamin and . Pierce, Types and Programming Languages, pp.153-170, 2002.

C. Bach-poulsen, P. Néron, A. Tolmach, and E. Visser, Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics, Leibniz International Proceedings in Informatics (LIPIcs), vol.56, 2016.

, , vol.20

C. Bach-poulsen, A. Rouvoet, A. Tolmach, R. Krebbers, and E. Visser, Intrinsically-typed definitional interpreters for imperative languages, Proceedings of the ACM on Programming Languages, vol.2, issue.POPL, pp.1-34, 2018.

J. Reynolds, Towards a theory of type structure, Lecture Notes in Computer Science, vol.19, pp.408-425, 1974.

M. Roberson, M. Harries, P. T. Darga, and C. Boyapati, Efficient software model checking of soundness of type systems, ACM SIGPLAN Notices, vol.43, issue.10, pp.493-504, 2008.

G. Ro?u and . Traian-florin-?erb?nu??, An Overview of the K Semantic Framework, Journal of Logic and Algebraic Programming, vol.79, pp.397-434, 2010.

A. Rouvoet, C. Bach-poulsen, R. Krebbers, and E. Visser, Intrinsically-typed definitional interpreters for linear, session-typed languages, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, vol.2020, pp.284-298, 2020.

C. Schürmann, Automating the Meta Theory of Deductive Systems, 2000.

C. Schwaab and J. G. Siek, Modular type-safety proofs in Agda, Proceedings of the 7th workshop on Programming languages meets program verification - PLPV '13, pp.3-12, 2013.

P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge et al., Ott, Proceedings of the 2007 ACM SIGPLAN international conference on Functional programming - ICFP '07, pp.1-12, 2007.

J. G. Siek and R. Garcia, Interpretations of the gradually-typed lambda calculus, Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming - Scheme '12, pp.81-92, 2012.

E. Visser, G. Wachsmuth, A. Tolmach, P. Neron, V. Vergu et al., A Language Designer's Workbench, Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software - Onward! '14, pp.95-111, 2014.

W. L. Schmitt, Walter Rathbone Bacon Traveling Scholarship Expedition to the West Coast of South America, 1926-1927 : Diary, Vol. 3, November 27, 1926 - January 16, 1927, SLE'20, 1926.

E. Visser, G. Wachsmuth, A. Tolmach, P. Neron, V. Vergu et al., A Language Designer's Workbench, Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software - Onward! '14, 2014.

M. Voelter and K. Solomatov, Software Language Engineering, Third International Conference on Software Language Engineering (SLE 2010) (Lecture Notes in Computer Science), 2011.

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.