Featherweight Java

Featherweight Java: A minimal core calculus for Java and GJ. Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational ”feel,” providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java’s. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.

References in zbMATH (referenced in 61 articles )

Showing results 1 to 20 of 61.
Sorted by year (citations)

1 2 3 4 next

  1. Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
  2. Capriccioli, Andrea; Servetto, Marco; Zucca, Elena: An imperative pure calculus (2016)
  3. von Rhein, Alexander; Thüm, Thomas; Schaefer, Ina; Liebig, Jörg; Apel, Sven: Variability encoding: from compile-time to load-time variability (2016)
  4. Damiani, Ferruccio; Viroli, Mirko: Type-based self-stabilisation for computational fields (2015)
  5. Dovland, Johan; Johnsen, Einar Broch; Owe, Olaf; Yu, Ingrid Chieh: A proof system for adaptable class hierarchies (2015)
  6. AbdelGawad, Moez A.: A domain-theoretic model of nominally-typed object-oriented programming (2014)
  7. Choi, Kwanghoon; Chang, Byeong-Mo: A type and effect system for activation flow of components in android programs (2014)
  8. Damiani, Ferruccio; Dovland, Johan; Broch Johnsen, Einar; Schaefer, Ina: Verifying traits: an incremental proof system for fine-grained reuse (2014)
  9. Rowe, Reuben N.S.; van Bakel, S.J.: Semantic types and approximation for featherweight Java (2014)
  10. Van Cutsem, Tom; Gonzalez Boix, Elisa; Scholliers, Christophe; Lombide Carreton, Andoni; Harnie, Dries; Pinte, Kevin; De Meuter, Wolfgang: Ambienttalk: programming responsive mobile peer-to-peer applications with actors (2014)
  11. Beringer, Lennart; Grabowski, Robert; Hofmann, Martin: Verifying pointer and string analyses with region type systems (2013)
  12. Bettini, Lorenzo; Capecchi, Sara; Damiani, Ferruccio: On flexible dynamic trait replacement for Java-like languages (2013)
  13. Bettini, Lorenzo; Damiani, Ferruccio; Schaefer, Ina: Compositional type checking of delta-oriented software product lines (2013)
  14. Bettini, Lorenzo; Damiani, Ferruccio; Schaefer, Ina; Strocco, Fabio: TraitRecordJ: a programming language with traits and records (2013)
  15. Lievens, David; Harrison, William: Abstraction over implementation structure with symmetrically encapsulated multimethods (2013)
  16. Saito, Chieri; Igarashi, Atsushi: Matching MyType to subtyping (2013)
  17. Viroli, Mirko; Beal, Jacob; Usbeck, Kyle: Operational semantics of proto (2013)
  18. Johnsen, Einar Broch; Mai Thuong Tran, Thi; Owe, Olaf; Steffen, Martin: Safe locking for multi-threaded Java with exceptions (2012)
  19. Lagorio, Giovanni; Servetto, Marco; Zucca, Elena: Featherweight Jigsaw. Replacing inheritance by composition in Java-like languages (2012)
  20. Ancona, Davide; Lagorio, Giovanni: Idealized coinductive type systems for imperative object-oriented programs (2011)

1 2 3 4 next