Open AccessTowards an Extrinsic Formalization of Featherweight Java in Agda
Author(s) -
Samuel da Silva Feitosa,
Rodrigo Ribeiro,
André Rauber Du Bois
Publication year - 2021
Publication title -
clei electronic journal
Language(s) - English
Resource type - Journals
ISSN - 0717-5000
DOI - 10.19153/cleiej.24.3.3
Subject(s) - programming language , computer science , java , semantics (computer science) , generics in java , software engineering , real time java , java annotation
Featherweight Java is one of the most popular calculi which specify object-oriented programming features. It has been used as the basis for investigating novel language functionalities, as well as to specify and understand the formal properties of existing features for languages in this paradigm. However, when considering mechanized formalization, it is hard to find an implementation for languages with complex structures and binding mechanisms as Featherweight Java. In this paper we formalize Featherweight Java, implementing the static and dynamic semantics in Agda, and proving the main safety properties for this calculus.