Sciweavers

Share
LFCS
2009
Springer

The Logic of Proofs as a Foundation for Certifying Mobile Computation

8 years 11 months ago
The Logic of Proofs as a Foundation for Certifying Mobile Computation
We explore an intuitionistic fragment of Art¨emov’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 normalization n-time system based on an abstract machine.
Eduardo Bonelli, Federico Feller
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where LFCS
Authors Eduardo Bonelli, Federico Feller
Comments (0)
books