Towards an extrinsic formalization of featherweight Java in Agda.

Feitosa, Samuel da Silva; Ribeiro, Rodrigo Geraldo; Bois, André Rauber Du

Use este identificador para citar ou linkar para este item: http://www.repositorio.ufop.br/jspui/handle/123456789/15837

Título:	Towards an extrinsic formalization of featherweight Java in Agda.
Autor(es):	Feitosa, Samuel da Silva Ribeiro, Rodrigo Geraldo Bois, André Rauber Du
Palavras-chave:	Mechanized semantics Type safety
Data do documento:	2020
Referência:	FEITOSA, S. da S.; RIBEIRO, R. G.; BOIS, A. R. D. Towards an extrinsic formalization of featherweight Java in Agda. CLEI Eletronic Journal, v. 24, n. 3, 2021. Disponível em: <http://www.clei.org/cleiej/index.php/cleiej/article/view/520>. Acesso em: 06 jul. 2022.
Resumo:	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.
URI:	http://www.repositorio.ufop.br/jspui/handle/123456789/15837
DOI:	https://doi.org/10.19153/cleiej.24.3.3
ISSN:	0717-5000
Licença:	This work is licensed under a Creative Commons Attribution 4.0 International License. Fonte: Clei Eletronic Journal. <http://www.clei.org/cleiej/index.php/cleiej/article/view/520>. Acesso em: 28 set. 2022.
Aparece nas coleções:	DECOM - Artigos publicados em periódicos

Arquivos associados a este item:

Arquivo	Descrição	Tamanho	Formato
ARTIGO_TowardsExtrinsicFormalization.pdf		397,7 kB	Adobe PDF	Visualizar/Abrir

Mostrar registro completo do item Visualizar estatísticas