Skip to main content
SpringerLink
Log in

Type-Directed Concurrency

  • Conference paper
CONCUR 2005 – Concurrency Theory (CONCUR 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3653))

Included in the following conference series:

  • 689 Accesses

Abstract

We introduce a novel way to integrate functional and concurrent programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as computation. The concurrent core arises from interpreting proof search as computation. The two are tightly integrated via a monad that permits both sides to share the same logical meaning for the linear connectives while preserving their different computational paradigms. For example, concurrent computation synthesizes proofs which can be evaluated as functional programs. We illustrate our design with some small examples, including an encoding of the pi-calculus.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. CLL implementation, Available electronically from http://www.cs.cmu.edu/~dg

  2. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. of POPL 2001, pp. 104–115 (2001)

    Google Scholar 

  3. Abramsky, S.: Computational interpretations of linear logic. Theoretical Computer Science 111(1–2), 3–57 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  4. Abramsky, S., Gay, S., Nagarajan, R.: Specification structures and propositionsas-types for concurrency. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043. Springer, Heidelberg (1996)

    Google Scholar 

  5. Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3), 297–347 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  6. Andreoli, J.-M., Pareschi, R.: Communication as fair distribution of knowledge. Technical Report ECRC-91-12, European Computer-Industry Research Centre (1991)

    Google Scholar 

  7. Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science 96, 217–248 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  8. Boudol, G.: Asynchrony and the pi-calculus. Technical Report RR-1702, INRIA SofiaAntipolis (1992)

    Google Scholar 

  9. Conchon, S., Fessant, F.L.: Jocaml: Mobile agents for objective-caml. In: Proc. of ASAMA 1999. IEEE Computer Society, Los Alamitos (1999)

    Google Scholar 

  10. Garg, D.: CLL: A concurrent language built from logical principles. Technical Report CMU-CS-05-104, Computer Science Department, Carnegie Mellon University (January 2005)

    Google Scholar 

  11. Giacalone, A., Mishra, P., Prasad, S.: Facile: A symmetric integration of concurrent and functional programming. International Journal of Parallel Programming 18(2), 121–160 (1989)

    Article  Google Scholar 

  12. Girard, J.-Y.: Linear logic. Theoretical Computer Science 5 (1987)

    Google Scholar 

  13. Jones, S.P., Gordon, A., Finne, S.: Concurrent Haskell. In: Proc. of POPL 1996 (1996)

    Google Scholar 

  14. López, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: Proc. of PPDP 2005 (2005) (to appear)

    Google Scholar 

  15. Nygaard, M., Winskel, G.: Domain theory for concurrency. Theor. Comput. Sc. 316(1-3) (2004)

    Google Scholar 

  16. Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Struc. in Comp. Sci. 11(4), 511–540 (2001)

    MATH  MathSciNet  Google Scholar 

  17. Pierce, B.C., Turner, D.N.: Pict: a programming language based on the picalculus. In: Proof, language, and interaction: essays in honour of Robin Milner, pp. 455–494. MIT Press, Cambridge (2000)

    Google Scholar 

  18. Reppy, J.H.: CML: A higher-order concurrent language. In: Proc. of PLDI 1991 (1991)

    Google Scholar 

  19. Reppy, J.H.: Concurrent programming in ML. Cambridge University Press, Cambridge (1999)

    Book  Google Scholar 

  20. Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes, ch. 15–17. Cambridge University Press, Cambridge (2001)

    Google Scholar 

  21. Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework I: Judgements and properties. Technical Report CMU-CS-02-101, Computer Science Department, Carnegie Mellon University (May 2003)

    Google Scholar 

  22. Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proc. of POPL 1999 (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University,  

    Deepak Garg & Frank Pfenning

Authors
  1. Deepak Garg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frank Pfenning
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of California, Santa Cruz

    Martín Abadi

  2. University of California, Santa Cruz, USA

    Luca de Alfaro

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Garg, D., Pfenning, F. (2005). Type-Directed Concurrency. In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 – Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_5

Download citation

  • DOI: https://doi.org/10.1007/11539452_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28309-6

  • Online ISBN: 978-3-540-31934-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation