Mechanized metatheory for a λ-calculus with trust types.

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

Título:	Mechanized metatheory for a λ-calculus with trust types.
Autor(es):	Ribeiro, Rodrigo Geraldo Figueiredo, Lucília Camarão de Figueiredo, Carlos Camarão de
Palavras-chave:	Type systems Proof assistants Soundness proofs
Data do documento:	2013
Referência:	RIBEIRO, R. G.; FIGUEIREDO, L. C. de; FIGUEIREDO, C. C. de. Mechanized metatheory for a λ-calculus with trust types. Journal of the Brazilian Computer Society, v. 19, n. 4, p. 433-443, nov. 2013. Disponível em: <https://link.springer.com/article/10.1007/s13173-013-0119-5>. Acesso em: 23 jan. 2017.
Resumo:	As computer programs become increasingly complex, techniques for ensuring trustworthiness of information manipulated by them become critical. In this work, we use the Coq proof assistant to formalise a λ-calculus with trust types, originally formulated by Ørbæk and Palsberg. We give formal proofs of type soundness, erasure and simulation theorems and also prove decidability of the typing problem. As a result of our formalisation a certified type checker is derived.
URI:	http://www.repositorio.ufop.br/handle/123456789/7173
Link para o artigo:	https://link.springer.com/article/10.1007/s13173-013-0119-5
DOI:	https://doi.org/10.1007/s13173-013-0119-5
ISSN:	1678-4804
Aparece nas coleções:	DECOM - Artigos publicados em periódicos

Arquivos associados a este item:

Arquivo	Descrição	Tamanho	Formato
ARTIGO_MechanizedMetatheoryCalculus.pdf Until 2030-01-23		1,71 MB	Adobe PDF	Visualizar/Abrir