Towards an Extrinsic Formalization of Featherweight Java in Agda

Authors

  • Samuel Feitosa Instituto Federal de Santa Catarina
  • Rodrigo Geraldo Ribeiro
  • Andre Rauber Du Bois

DOI:

https://doi.org/10.19153/cleiej.24.3.3

Keywords:

Featherweight Java, Mechanized Semantics, Type Safety

Abstract

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.

Downloads

Published

2021-12-20

Issue

Vol. 24 No. 3 (2021): Regular papers and Special Issue For Digital Healthcare

Section

Articles

License

Copyright (c) 2021 Samuel Feitosa, Rodrigo Geraldo Ribeiro, Andre Rauber Du Bois

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).