Proof-Carrying Code in a Session-Typed Process Calculus

  • Frank Pfenning
  • Luis Caires
  • Bernardo Toninho
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)


Dependent session types allow us to describe not only properties of the I/O behavior of processes but also of the exchanged data. In this paper we show how to exploit dependent session types to express proof-carrying communication. We further introduce two modal operators into the type theory to provide detailed control about how much information is communicated: one based on traditional proof irrelevance and one integrating digital signatures.


Process calculus session types proof irrelevance proof-carrying code 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Avijit, K., Datta, A., Harper, R.: Distributed programming with distributed authorization. In: Proceedings of the 5th Workshop on Types in Language Design and Implementation, TLDI 2010, pp. 27–38. ACM, New York (2010)Google Scholar
  2. 2.
    Awodey, S., Bauer, A.: Propositions as [types]. Journal of Logic and Computation 14(4), 447–471 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: 21st Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, pp. 17–32. IEEE Computer Society (June 2008)Google Scholar
  4. 4.
    Bonelli, E., Compagnoni, A., Gunter, E.L.: Correspondence Assertions for Process Synchronization in Concurrent Communications. J. of Func. Prog. 15(2), 219–247 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Caires, L., Pfenning, F.: Session Types as Intuitionistic Linear Propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Dezani-Ciancaglini, M., de’Liguoro, U.: Sessions and Session Types: An Overview. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol. 6194, pp. 1–28. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Garg, D., Bauer, L., Bowers, K.D., Pfenning, F., Reiter, M.K.: A Linear Logic of Authorization and Knowledge. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 297–312. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Garg, D., Pfenning, F.: A proof-carrying file system. In: Evans, D., Vigna, G. (eds.) Proceedings of the 31st Symposium on Security and Privacy (Oakland 2010), Berkeley, California. IEEE (May 2010); Extended version available as Technical Report CMU-CS-09-123 (June 2009)Google Scholar
  9. 9.
    Honda, K.: Types for Dyadic Interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)Google Scholar
  10. 10.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Mazurak, K., Zdancewic, S.: Lolliproc: To concurrency from classical linear logic via Curry-Howard and control. In: Hudak, P., Weirich, S. (eds.) Proceedings of the 15th International Conference on Functional Programming (ICFP 2010), Baltimore, Maryland, pp. 39–50. ACM (September 2010)Google Scholar
  12. 12.
    Necula, G.C.: Proof-carrying code. In: Jones, N.D. (ed.) Conference Record of the 24th Symposium on Principles of Programming Languages (POPL 1997), Paris, France, pp. 106–119. ACM Press (January 1997)Google Scholar
  13. 13.
    Necula, G.C., Lee, P.: Safe kernel extensions without run-time checking. In: Proceedings of the Second Symposium on Operating System Design and Implementation (OSDI 1996), Seattle, Washington, pp. 229–243 (October 1996)Google Scholar
  14. 14.
    Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: Halpern, J. (ed.) Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001), Boston, Massachusetts, pp. 221–230. IEEE (June 2001)Google Scholar
  15. 15.
    Salvesen, A., Smith, J.M.: The strength of the subset type in Martin-Löf’s type theory. In: 3rd Annual Symposium on Logic in Computer Science (LICS 1988), Edinburgh, Scotland, pp. 384–391. IEEE (July 1988)Google Scholar
  16. 16.
    Swamy, N., Checn, J., Fournet, C., Strub, P.-Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: Danvy, O. (ed.) International Conference on Functional Programming (ICFP 2011), Tokyo, Japan. ACM (September 2011) (to appear)Google Scholar
  17. 17.
    Swamy, N., Chen, J., Chugh, R.: Enforcing Stateful Authorization and Information Flow Policies in Fine. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 529–549. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  18. 18.
    Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Proceedings of the 13th International Symposium on Principles and Practice of Declarative Programming (PPDP 2011), pp. 161–172. ACM ( July 2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Frank Pfenning
    • 1
  • Luis Caires
    • 2
  • Bernardo Toninho
    • 1
    • 2
  1. 1.Computer Science DepartmentCarnegie Mellon UniversityPittsburghUSA
  2. 2.Faculdade de Ciencias e TecnologiaUniversidade Nova de LisboaLisboaPortugal

Personalised recommendations