×

zbMATH — the first resource for mathematics

Implementing type systems for the IDE with Xsemantics. (English) Zbl 1348.68030
Summary: Xsemantics is a DSL for writing type systems, reduction rules and, in general, relation rules for languages implemented in Xtext (Xtext is an Eclipse framework for rapidly building languages together with all the typical IDE tooling). Xsemantics aims at reducing the gap between the formalization of a language (i.e., type system and operational semantics) and the actual implementation in Xtext, since it uses a syntax that resembles the rules in a formal setting. In this paper we present the main features of Xsemantics for implementing type systems and reduction rules through examples (Featherweight Java and lambda calculus). We show how such implementations are close to the actual formalizations, and how Xsemantics can be a helpful tool when proving the type safety of a language. We also describe the new features of Xsemantics that help achieving a modular and efficient implementation of type systems. In particular, we focus on specific implementation techniques for implementing type systems that are suited for the IDE (in our context, Eclipse), in order to keep the tooling responsive and guarantee a good user experience.
MSC:
68N18 Functional programming and lambda calculus
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DLTK
[2] Xtext
[3] Draft ECMAScript language specification. Working draft ECMA-262, 6th edition, Rev. 24, Apr. 27, 2014, ISO/IEC, Apr. 2014.
[4] Batory, D.; Lofaso, B.; Smaragdakis, Y., JTS: tools for implementing domain-specific languages, (ICSR, (1998), IEEE), 143-153
[5] Bertot, Y.; Castéran, P. P., Interactive theorem proving and program development: coq’art: the calculus of inductive constructions, Texts Theoret. Comput. Sci., (2004), Springer · Zbl 1069.68095
[6] Bettini, L., A DSL for writing type systems for xtext languages, (PPPJ, (2011), ACM), 31-40
[7] Bettini, L., Implementing domain-specific languages with xtext and xtend, (2013), Packt Publishing
[8] Bettini, L., Implementing Java-like languages in xtext with xsemantics, (OOPS (SAC), (2013), ACM), 1559-1564
[9] Bettini, L.; Stoll, D.; Völter, M.; Colameo, S., Approaches and tools for implementing type systems in xtext, (SLE, Lect. Notes Comput. Sci., vol. 7745, (2012), Springer), 392-412
[10] Borras, P.; Clement, D.; Despeyroux, T.; Incerpi, J.; Kahn, G.; Lang, B.; Pascual, V., CENTAUR: the system, Software Engineering Symposium on Practical Software Development Environments, ACM SIGPLAN Not., 24, 14-24, (1988)
[11] Bracha, G., Pluggable type systems, (Workshop on Revival of Dynamic Languages, (2004))
[12] van den Brand, M. G.J.; Heering, J.; Klint, P.; Olivier, P. A., Compiling language definitions: the ASF+SDF compiler, ACM TOPLAS, 24, 4, 334-368, (2002)
[13] Bravenboer, M.; de Groot, R.; Visser, E., Metaborg in action: examples of domain-specific language embedding and assimilation using stratego/XT, (GTTSE, Lect. Notes Comput. Sci., vol. 4143, (2006), Springer), 297-311
[14] Bravenboer, M.; Kalleberg, K. T.; Vermaas, R.; Visser, E., Stratego/XT 0.17. A language and toolset for program transformation, Sci. Comput. Program., 72, 1-2, 52-70, (2008)
[15] Cameron, N.; Ernst, E.; Drossopoulou, S., Towards an existential types model for Java wildcards, (Formal Techniques for Java-like Programs (FTfJP) 2007, (July 2007))
[16] Cardelli, L., Type systems, ACM Comput. Surv., 28, 1, 263-264, (1996)
[17] Cazzola, W.; Vacchi, E., Neverlang 2: componentised language development for the JVM, (Software Composition, Lect. Notes Comput. Sci., vol. 8088, (2013), Springer), 17-32
[18] Charles, P.; Fuhrer, R.; Sutton, S.; Duesterwald, E.; Vinju, J., Accelerating the creation of customized, language-specific IDEs in eclipse, (OOPSLA, (2009), ACM), 191-206
[19] Clark, T.; Sammut, P.; Willans, J., Superlanguages, developing languages and applications with XMF, (2008), Ceteva
[20] Damas, L.; Milner, R., Principal type schemes for functional programs, (POPL, (1982), ACM), 207-212
[21] Dart Team, Dart programming language specification, (Mar. 2014), 1.2 edition
[22] Despeyroux, T., Typol: a formalism to implement natural semantics, (Mar. 1988), INRIA, Technical Report 94
[23] Dijkstra, A.; Swierstra, S. D., Ruler: programming type rules, (FLOPS, Lect. Notes Comput. Sci., vol. 3945, (2006), Springer), 30-46 · Zbl 1185.68191
[24] Efftinge, S.; Eysholdt, M.; Köhnlein, J.; Zarnekow, S.; Hasselbring, W.; von Massow, R., Xbase: implementing domain-specific languages for Java, (GPCE, (2012), ACM), 112-121
[25] Ekman, T.; Hedin, G., The jastadd system - modular extensible compiler construction, Sci. Comput. Program., 69, 1-3, 14-26, (2007) · Zbl 1147.68437
[26] Erdweg, S.; van der Storm, T.; Völter, M.; Tratt, L.; Bosman, R.; Cook, W. R.; Gerritsen, A.; Hulshout, A.; Kelly, S.; Loh, A.; Konat, G.; Molina, P. J.; Palatnik, M.; Pohjonen, R.; Schindler, E.; Schindler, K.; Solmi, R.; Vergu, V.; Visser, E.; van der Vlist, K.; Wachsmuth, G.; van der Woning, J., Evaluating and comparing language workbenches: existing results and benchmarks for the future, Comput. Lang. Syst. Struct., 44A, (2015)
[27] Eysholdt, M.; Behrens, H., Xtext: implement your language faster than the quick and dirty way, (SPLASH/OOPSLA Companion, (2010), ACM), 307-309
[28] Felleisen, M.; Findler, R. B.; Flatt, M., Semantics engineering with PLT redex, (2009), The MIT Press Cambridge, MA · Zbl 1183.68359
[29] Fowler, M., A language workbench in action - MPS, (2008)
[30] Gordon, M., From LCF to HOL: a short history, (Proof, Language, and Interaction: Essays in Honour of Robin Milner, (2000), The MIT Press), 169-186
[31] Gosling, J.; Joy, B.; Steele, G.; Bracha, G.; Buckley, A., The Java language specification, Java SE 7 edition, (2013), Addison-Wesley
[32] Hage, J.; Heeren, B., Strategies for solving constraints in type and effect systems, (VODCA, Electron. Notes Theor. Comput. Sci., vol. 236, (2009), Elsevier), 163-183
[33] Heeren, B.; Hage, J.; Swierstra, S. D., Scripting the type inference process, (Eighth International Conference on Functional Programming, (2003), ACM Press), 3-13 · Zbl 1315.68050
[34] Heidenreich, F.; Johannes, J.; Karol, S.; Seifert, M.; Wende, C., Derivation and refinement of textual syntax for models, (ECMDA-FA, Lect. Notes Comput. Sci., vol. 5562, (2009), Springer), 114-129
[35] Heiduk, A.; Skatulla, S., From spaghetti to xsemantics - practical experiences migrating typesystems for 12 languages, (2015), XtextCon
[36] Hejlsberg, A.; Lucco, S., Typescript language specification, (Apr. 2014), Microsoft, 1.0 edition
[37] Hindley, J. R., Basic simple type theory, (1987), Cambridge University Press
[38] Igarashi, A.; Nagira, H., Union types for object-oriented programming, J. Object Technol., 6, 2, (2007)
[39] Igarashi, A.; Pierce, B.; Wadler, P., Featherweight Java: a minimal core calculus for Java and GJ, ACM TOPLAS, 23, 3, 396-450, (2001)
[40] Jouault, F.; Bézivin, J.; Kurtev, I., TCS: a DSL for the specification of textual concrete syntaxes in model engineering, (GPCE, (2006), ACM), 249-254
[41] Kahn, G.; Lang, B.; Melese, B.; Morcos, E., Metal: a formalism to specify formalisms, Sci. Comput. Program., 3, 2, 151-188, (1983)
[42] Kats, L. C.L.; Visser, E., The spoofax language workbench. rules for declarative specification of languages and ides, (OOPSLA, (2010), ACM), 444-463
[43] Klein, C.; Clements, J.; Dimoulas, C.; Eastlund, C.; Felleisen, M.; Flatt, M.; McCarthy, J. A.; Rafkind, J.; Tobin-Hochstadt, S.; Findler, R. B., Run your research: on the effectiveness of lightweight mechanization, (POPL, (2012), ACM), 285-296
[44] Konat, G.; Kats, L.; Wachsmuth, G.; Visser, E., Declarative name binding and scope rules, (SLE, Lect. Notes Comput. Sci., vol. 7745, (2012), Springer), 311-331
[45] Krahn, H.; Rumpe, B.; Völkel, S., Monticore: a framework for compositional development of domain specific languages, Int. J. Softw. Tools Technol. Transf., 12, 5, 353-372, (2010)
[46] Levine, J., Flex & bison, (2009), O’Reilly Media
[47] Morcos-Chounet, E.; Conchon, A., PPML: a general formalism to specify prettyprinting, (IFIP Congress, (1986)), 583-590
[48] Neron, P.; Tolmach, A. P.; Visser, E.; Wachsmuth, G., A theory of name resolution, (ESOP, Lect. Notes Comput. Sci., vol. 9032, (2015), Springer), 205-231 · Zbl 1335.68062
[49] Object Management Group, Object constraint language, (2010), version 2.2, OMG document number: formal/2010-02-01 edition
[50] Parr, T., The definitive ANTLR reference: building domain-specific languages, Pragmatic Programmers, (2007)
[51] Paulson, L. C., Isabelle: A generic theorem prover, Lect. Notes Comput. Sci., vol. 828, (1994), Springer · Zbl 0825.68059
[52] Pfeiffer, M.; Pichler, J., A comparison of tool support for textual domain-specific languages, (Proc. DSM, (2008)), 1-7
[53] Pierce, B. C., Types and programming languages, (2002), The MIT Press Cambridge, MA
[54] Prasanna, D. R., Dependency injection: design patterns using spring and guice, (2009), Manning
[55] Renggli, L.; Denker, M.; Nierstrasz, O., Language boxes: bending the host language with modular language changes, (SLE, Lect. Notes Comput. Sci., vol. 5969, (2009), Springer), 274-293
[56] Reps, T.; Teitelbaum, T., The synthesizer generator, (Software Engineering Symposium on Practical Software Development Environments, (1984), ACM), 42-48
[57] Robinson, J. A., Computational logic: the unification computation, Mach. Intell., 6, (1971)
[58] Rosu, G.; Serbanuta, T.-F., An overview of the K semantic framework, J. Log. Algebr. Program., 79, 6, 397-434, (2010) · Zbl 1214.68188
[59] Sewell, P.; Nardelli, F. Z.; Owens, S.; Peskine, G.; Ridge, T.; Sarkar, S.; Strnisa, R., Ott: effective tool support for the working semanticist, J. Funct. Program., 20, 1, 71-122, (2010) · Zbl 1185.68201
[60] Steinberg, D.; Budinsky, F.; Paternostro, M.; Merks, E., EMF: eclipse modeling framework, (2008), Addison-Wesley
[61] Vacchi, E.; Cazzola, W., Neverlang: a framework for feature-oriented language development, Comput. Lang. Syst. Struct., 43, 3, 1-40, (2015)
[62] Vergu, V. A.; Neron, P.; Visser, E., Dynsem: a DSL for dynamic semantics specification, (RTA, LIPIcs, vol. 36, (2015), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 365-378 · Zbl 1366.68015
[63] Visser, E.; Wachsmuth, G.; Tolmach, A. P.; Neron, P.; Vergu, V. A.; Passalaqua, A.; Konat, G., A language Designer’s workbench: a one-stop-shop for implementation and verification of language designs, (Onward!, (2014), ACM), 95-111
[64] Voelter, M., Language and IDE modularization and composition with MPS, (GTTSE, Lect. Notes Comput. Sci., vol. 7680, (2011), Springer), 383-430
[65] Voelter, M.; Benz, S.; Dietrich, C.; Engelmann, B.; Helander, M.; Kats, L. C.L.; Visser, E.; Wachsmuth, G., DSL engineering - designing, implementing and using domain-specific languages, (2013)
[66] Völter, M., Xtext/TS - a typesystem framework for xtext, (2011)
[67] Warmer, J.; Kleppe, A., The object constraint language: precise modeling with UML, (1999), Addison-Wesley
[68] Xu, H., Erilex: an embedded domain specific language generator, (TOOLS, Lect. Notes Comput. Sci., vol. 6141, (2010), Springer), 192-212
[69] Zarnekow, S., Xtext best practices, (2012)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.