Mechanized metatheory for a λ λ-calculus with trust types
Se ha publicado un artículo de razonamiento formalizado en Coq titulado Mechanized metatheory for a λ λ-calculus with trust types.
Sus autores son
- Rodrigo Ribeiro (de la Universidade Federal de Minas Gerais, Brasil),
- Carlos Camarão (de la Universidade Federal de Minas Gerais, Brasil) y
- Lucília Figueiredo (de la Universidade Federal de Ouro Preto, Brasil).
Su resumen es
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.
El código de las correspondientes teorías en Coq se encuentra aquí.
La versión final del trabajo se ha publicado en el Journal of the Brazilian Computer Society.