Paper

Type
ARTICLE  
Title
Implementing type systems for the IDE with Xsemantics  
Authors
Lorenzo Bettini 
Book
Journal of Logical and Algebraic Methods in Programming  
Pages
655 - 680  
Abstract
Abstract 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.  
Volume
85  
Number
5, Part 1  
Year
2016  
Bibtex key
Bettini2016  
Paper Url1
http://www.sciencedirect.com/science/article/pii/S235222081500142X  
Bibtex
@ARTICLE{Bettini2016,
  title = {{Implementing type systems for the IDE with Xsemantics}},
  author = {Bettini, Lorenzo},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  pages = {655 - 680},
  abstract = {Abstract 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.},
  volume = {85},
  number = {5, Part 1},
  year = {2016},
  url = {http://www.sciencedirect.com/science/article/pii/S235222081500142X},
  doi = {http://dx.doi.org/10.1016/j.jlamp.2015.11.005},
}
 
Created
2015-12-28 10:16:43  
Modified
2017-02-09 10:22:15