Abstract
We explore an intuitionistic fragment of Artëmov'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 for a run-time system based on an abstract machine. © Springer-Verlag Berlin Heidelberg 2009.
Cite
CITATION STYLE
Bonelli, E., & Feller, F. (2009). The logic of proofs as a foundation for certifying mobile computation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5407 LNCS, pp. 76–91). https://doi.org/10.1007/978-3-540-92687-0_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
