The logic of proofs as a foundation for certifying mobile computation

Título:

The logic of proofs as a foundation for certifying mobile computation

Autor:

Bonelli, Eduardo

Colaboradores:

; Feller, Federico

Temas:

COMPUTACIÓN MÓVILLENGUAJES DE PROGRAMACIÓNPROGRAMACIÓN LÓGICA

En:

Logical Foundations of Computer Science : International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings. Berlín : Springer, 2009. (Lecture Notes in Computer Science ; 5407), pp. 76-91

Resumen:

We explore an intuitionistic fragment of Artemov's Logic of Proofs as a type system for a programming language for mobile units. Such units consist of both a code and certificate component. Dubbed the Certifying Mobile Calculus, our language caters for both code and certificate development in a unified theory. In the same way that mobile code is constructed out of code components and extant type systems track local resource usage to ensure the mobile nature of these components, our system additionally ensures correct certificate construction out of certificate components. We present proofs of type safety and strong normalistion for a run-time system based on an abstract machine.

URL/DOI:

http://dx.doi.org/10.1007/978-3-540-92687-0_6

Medio:

Soporte electrónico

Tipo de documento:

Artículo

Descripción física:

1 archivo (293,4 KB)

Idioma:

Inglés

Publicación:

,  2009

Puede solicitar más fácilmente el ejemplar con: A0283

Ver estantes