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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Artëmov, S., Beklemishev, L.: Provability logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 13, pp. 189–360. Kluwer, Dordrecht (2004)
Artëmov, S.N., Bonelli, E.: The intensional lambda calculus. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 12–25. Springer, Heidelberg (2007)
Artemov, S.: Operational modal logic. Technical Report MSI 95-29, Cornell Univsersity (1995)
Artemov, S.: Explicit provability and constructive semantics. Bulletin of Symbolic Logic 7(1), 1–36 (2001)
Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics. Elsevier, Amsterdam (2006)
Bonelli, E., Feller, F.: The logic of proofs as a foundation for certifying mobile computation, http://www.lifia.info.unlp.edu.ar/~eduardo/lpCertFull.pdf
Borghuis, T., Feijs, L.M.G.: A constructive logic for services and information flow in computer networks. Comput. J. 43(4), 274–289 (2000)
Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP, pp. 233–243 (2000)
Davies, R., Pfenning, F.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11, 511–540 (2001)
Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555–604 (2001)
Herbelin, H.: A lambda-calculus structure isomorphic to gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61–75. Springer, Heidelberg (1995)
Jia, L., Walker, D.: Modal proofs as distributed programs (extended abstract). In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 219–233. Springer, Heidelberg (2004)
Moody, J.: Logical mobility and locality types. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol. 3573, pp. 69–84. Springer, Heidelberg (2005)
Murphy VII, T.: Modal Types for Mobile Code. PhD thesis, Carnegie Mellon (draft) (January 2008)
Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)
Taha, W., Sheard, T.: Multi-stage programming. In: ICFP, p. 321 (1997)
Murphy VII, T., Crary, K., Harper, R.: Distributed control flow with classical modal logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 51–69. Springer, Heidelberg (2005)
Murphy VII, T., Crary, K., Harper, R.: Type-safe distributed programming with ml5. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol. 4912, pp. 108–123. Springer, Heidelberg (2008)
Murphy VII, T., Crary, K., Harper, R., Pfenning, F.: A symmetric modal lambda calculus for distributed computing. In: LICS, pp. 286–295. IEEE Computer Society, Los Alamitos (2004)
Wickline, P., Lee, P., Pfenning, F., Davies, R.: Modal types as staging specifications for run-time code generation. ACM Comput. Surv. 30(3es), 8 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonelli, E., Feller, F. (2008). The Logic of Proofs as a Foundation for Certifying Mobile Computation. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2009. Lecture Notes in Computer Science, vol 5407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92687-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-92687-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-92686-3
Online ISBN: 978-3-540-92687-0
eBook Packages: Computer ScienceComputer Science (R0)