TY - JOUR
T1 - Justification Logic as a foundation for certifying mobile computation
AU - Bonelli, Eduardo
AU - Feller, Federico
PY - 2012/7
Y1 - 2012/7
N2 - We explore an intuitionistic fragment of Artëmov's . Justification Logic as a type system for a programming language for . mobile units. Such units consist of both a code and a certificate component. Our language, the . Certifying Mobile Calculus, caters for 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 . Justification Logic as a type system for a programming language for . mobile units. Such units consist of both a code and a certificate component. Our language, the . Certifying Mobile Calculus, caters for 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.
KW - Curry-de Bruijn-Howard isomorphism
KW - Justification Logic
KW - Mobile computation
KW - Typed lambda calculus
UR - http://www.scopus.com/inward/record.url?scp=84857361381&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84857361381&partnerID=8YFLogxK
U2 - 10.1016/j.apal.2011.09.007
DO - 10.1016/j.apal.2011.09.007
M3 - Article
AN - SCOPUS:84857361381
SN - 0168-0072
VL - 163
SP - 935
EP - 950
JO - Annals of Pure and Applied Logic
JF - Annals of Pure and Applied Logic
IS - 7
ER -