TY - GEN
T1 - The logic of proofs as a foundation for certifying mobile computation
AU - Bonelli, Eduardo
AU - Feller, Federico
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=67650504783&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=67650504783&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-92687-0_6
DO - 10.1007/978-3-540-92687-0_6
M3 - Conference contribution
AN - SCOPUS:67650504783
SN - 3540926860
SN - 9783540926863
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 76
EP - 91
BT - Logical Foundations of Computer Science - International Symposium, LFCS 2009, Proceedings
T2 - International Symposium on Logical Foundations of Computer Science, LFCS 2009
Y2 - 3 January 2009 through 6 March 2009
ER -