Skip to main content
SpringerLink
Log in

A Lambda Calculus for Gödel–Dummett Logic Capturing Waitfreedom

  • Conference paper
Book cover Functional and Logic Programming (FLOPS 2012)

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

Included in the following conference series:

Abstract

We propose a typed lambda calculus based on Avron’s hypersequent calculus for Gödel–Dummett logic. This calculus turns out to model waitfree computation. Besides strong normalization and non-abortfullness, we give soundness and completeness of the calculus against the typed version of waitfree protocols. The calculus is not only proof theoretically interesting, but also valuable as a basis for distributed programming languages.

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. Abramsky, S.: Computational interpretations of linear logic. Theo. Comp. Sci. 111(1-2), 3–57 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  2. Avron, A.: Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Artif. Intell. 4, 225–248 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  3. Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics, pp. 1–32. Clarendon Press (1996)

    Google Scholar 

  4. Baaz, M., Ciabattoni, A., Fermüller, C.: A natural deduction system for intuitionistic fuzzy logic. In: Lectures on Soft Computing (2001)

    Google Scholar 

  5. Balat, V., Di Cosmo, R., Fiore, M.: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. SIGPLAN Not. 39(1), 64–76 (2004)

    Article  Google Scholar 

  6. Biran, O., Moran, S., Zaks, S.: A combinatorial characterization of the distributed tasks which are solvable in the presence of one faulty processor. In: PODC 1988, pp. 263–275. ACM (1988)

    Google Scholar 

  7. Borowsky, E., Gafni, E.: Immediate atomic snapshots and fast renaming. In: PODC 1993, pp. 41–51. ACM (1993)

    Google Scholar 

  8. Ciabattoni, A., Galatos, N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: LICS 2008, pp. 229–240. IEEE (2008)

    Google Scholar 

  9. Dummett, M.: A propositional calculus with denumerable matrix. J. Symb. Logic 24(2), 97–106 (1959)

    Article  MathSciNet  MATH  Google Scholar 

  10. Fermüller, C.G.: Parallel Dialogue Games and Hypersequents for Intermediate Logics. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol. 2796, pp. 48–64. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Fournet, C., Gonthier, G.: The Join Calculus: A Language for Distributed Mobile Programming. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 268–332. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. Gentzen, G.: Investigations into logical deduction. American Philosophical Quarterly 1(4), 288–306 (1964)

    Google Scholar 

  13. de Groote, P.: On the Strong Normalisation of Intuitionistic Natural Deduction with Permutation-Conversions. Information and Computation 178(2), 441–464 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  14. Herlihy, M.: Impossibility and universality results for wait-free synchronization. In: PODC 1988, pp. 276–290. ACM (1988)

    Google Scholar 

  15. Hirai, Y.: An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 272–289. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Honda, K., Tokoro, M.: An Object Calculus for Asynchronous Communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  17. Milner, R.: Communicating and mobile systems: the pi-calculus. Cambridge University Press (1999)

    Google Scholar 

  18. Moran, S.: Extended impossibility results for asynchronous complete networks. Information Processing Letters 26(3), 145–151 (1987)

    Article  MathSciNet  Google Scholar 

  19. Saks, M., Zaharoglou, F.: Wait-free k-set agreement is impossible: the topology of public knowledge. In: STOC 1993, pp. 101–110. ACM (1993)

    Google Scholar 

  20. Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry–Howard isomorphism. Elsevier (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. JSPS, The University of Tokyo, Japan

    Yoichi Hirai

Authors
  1. Yoichi Hirai
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Applied Mathematics and Computer Science, Ghent University, Krijgslaan 281 S9 WE02, 9000, Ghent, Belgium

    Tom Schrijvers

  2. Dept. of Computer Science, University of Freiburg, Georges-Köhler-Allee 106, 79110, Freiburg, Germany

    Peter Thiemann

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hirai, Y. (2012). A Lambda Calculus for Gödel–Dummett Logic Capturing Waitfreedom. In: Schrijvers, T., Thiemann, P. (eds) Functional and Logic Programming. FLOPS 2012. Lecture Notes in Computer Science, vol 7294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29822-6_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-29822-6_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-29821-9

  • Online ISBN: 978-3-642-29822-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation