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 |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.