Montagu, Jeremy, SLE'20, 2020. ,
SASyLF, Proceedings of the 2008 international workshop on Functional and declarative programming in education - FDPE '08, pp.31-40, 2008. ,
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
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. ,
Type Systems, Computer Science Handbook, pp.2327-2358, 2004. ,
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 formulation of the simple theory of types, Journal of Symbolic Logic, vol.5, issue.2, pp.56-68, 1940. ,
, , 2015.
Early Experience in Teaching the Basics of Functional Language Design with a Language Type Checker, Lecture Notes in Computer Science, pp.21-37, 2020. ,
Meta-theory à la carte, Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13, pp.207-218, 2013. ,
,
Developing an Eclipse editor for MARC records using Xtext, Software: Practice and Experience, vol.43, issue.11, pp.1377-1392, 2012. ,
SugarJ, Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications - OOPSLA '11, pp.391-406, 2011. ,
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
Typed programming languages, Transitions and Trees, vol.1816, pp.185-210 ,
Evaluating and comparing language workbenches, Computer Languages, Systems & Structures, vol.44, pp.24-47, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01261481
Semantics Engineering with PLT Redex, 2009. ,
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. ,
Automating Type Soundness Proofs for Domain-Specific Languages, 2019. ,
Using Vampire in Soundness Proofs of Type Systems, Proceedings of the 1st and 2nd ,
Using Vampire in Soundness Proofs of Type Systems, Vampire Workshops (EPiC Series in Computing, vol.38, pp.33-51 ,
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 ,
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. ,
Practical Foundations for Programming Languages, 2009. ,
A Type-Theoretic Interpretation of Standard ML, Proof, Language, and Interaction, 2000. ,
Featherweight Java, ACM Transactions on Programming Languages and Systems, vol.23, issue.3, pp.396-450, 2001. ,
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. ,
Sound type-dependent syntactic language extension, ACM SIGPLAN Notices, vol.51, issue.1, pp.204-216, 2016. ,
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. ,
Lem, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming - ICFP '14, pp.175-188, 2014. ,
A Theory of Name Resolution, Programming Languages and Systems, vol.9032, pp.205-231, 2015. ,
Functional Big-Step Semantics, Programming Languages and Systems, vol.9632, pp.589-615, 2016. ,
System Description: Twelf ? A Meta-Logical Framework for Deductive Systems, Automated Deduction ? CADE-16, pp.202-206, 1999. ,
Types and Programming Languages, pp.153-170, 2002. ,
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics, Leibniz International Proceedings in Informatics (LIPIcs), vol.56, 2016. ,
, , vol.20
Intrinsically-typed definitional interpreters for imperative languages, Proceedings of the ACM on Programming Languages, vol.2, issue.POPL, pp.1-34, 2018. ,
Towards a theory of type structure, Lecture Notes in Computer Science, vol.19, pp.408-425, 1974. ,
Efficient software model checking of soundness of type systems, ACM SIGPLAN Notices, vol.43, issue.10, pp.493-504, 2008. ,
An Overview of the K Semantic Framework, Journal of Logic and Algebraic Programming, vol.79, pp.397-434, 2010. ,
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. ,
Automating the Meta Theory of Deductive Systems, 2000. ,
Modular type-safety proofs in Agda, Proceedings of the 7th workshop on Programming languages meets program verification - PLPV '13, pp.3-12, 2013. ,
Ott, Proceedings of the 2007 ACM SIGPLAN international conference on Functional programming - ICFP '07, pp.1-12, 2007. ,
Interpretations of the gradually-typed lambda calculus, Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming - Scheme '12, pp.81-92, 2012. ,
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. ,
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. ,
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. ,
Software Language Engineering, Third International Conference on Software Language Engineering (SLE 2010) (Lecture Notes in Computer Science), 2011. ,
A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994. ,