Normal view MARC view ISBD view

The logic of proofs as a foundation for certifying mobile computation

By:

Bonelli, Eduardo

Contributor(s):

Feller, Federico

Material type: Article

ArticlePublication details: ref_localidad@NULL : , 2009Description: 1 archivo (293,4 KB)Subject(s):

Online resources:

Summary: 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.

Tags from this library: No tags from this library for this title. Log in to add tags.

Average rating: 0.0 (0 votes)

Holdings
Item type	Current library	Call number	Status	Date due	Barcode
Capítulo de libro	Biblioteca Fac.Informática	A0283 (Browse shelf(Opens below))	Available		DIF-A0283

Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática - UNLP (Colección BIPA/Biblioteca)

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.

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

There are no comments on this title.

to post a comment.