Por favor, use este identificador para citar o enlazar este ítem:
http://www.repositorio.ufop.br/jspui/handle/123456789/7173
Título : | Mechanized metatheory for a λ-calculus with trust types. |
Autor : | Ribeiro, Rodrigo Geraldo Figueiredo, Lucília Camarão de Figueiredo, Carlos Camarão de |
Palabras clave : | Type systems Proof assistants Soundness proofs |
Fecha de publicación : | 2013 |
Citación : | 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. |
Resumen : | 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 |
metadata.dc.identifier.uri2: | https://link.springer.com/article/10.1007/s13173-013-0119-5 |
metadata.dc.identifier.doi: | https://doi.org/10.1007/s13173-013-0119-5 |
ISSN : | 1678-4804 |
Aparece en las colecciones: | DECOM - Artigos publicados em periódicos |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | |
---|---|---|---|---|
ARTIGO_MechanizedMetatheoryCalculus.pdf Until 2030-01-23 | 1,71 MB | Adobe PDF | Visualizar/Abrir |
Los ítems de DSpace están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.