Mechanized metatheory for a λ-calculus with trust types.

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.creatorRibeiro, Rodrigo Geraldo-
Autor(es): dc.creatorFigueiredo, Lucília Camarão de-
Autor(es): dc.creatorFigueiredo, Carlos Camarão de-
Data de aceite: dc.date.accessioned2025-08-21T15:28:50Z-
Data de disponibilização: dc.date.available2025-08-21T15:28:50Z-
Data de envio: dc.date.issued2017-02-01-
Data de envio: dc.date.issued2017-02-01-
Data de envio: dc.date.issued2013-
Fonte completa do material: dc.identifierhttp://www.repositorio.ufop.br/handle/123456789/7173-
Fonte completa do material: dc.identifierhttps://link.springer.com/article/10.1007/s13173-013-0119-5-
Fonte completa do material: dc.identifierhttps://doi.org/10.1007/s13173-013-0119-5-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/1016230-
Descrição: dc.descriptionAs 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.-
Formato: dc.formatapplication/pdf-
Idioma: dc.languageen-
Direitos: dc.rightsaberto-
Palavras-chave: dc.subjectType systems-
Palavras-chave: dc.subjectProof assistants-
Palavras-chave: dc.subjectSoundness proofs-
Título: dc.titleMechanized metatheory for a λ-calculus with trust types.-
Aparece nas coleções:Repositório Institucional - UFOP

Não existem arquivos associados a este item.