Skip to main content

An Adequate, Denotational, Functional-Style Semantics for Typed FlatCurry

  • Conference paper

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

Abstract

With the aim of putting type-based reasoning for functional logic languages, as recently explored by [5], on a formal basis, we develop a denotational semantics for a typed core language of Curry. Dealing with the core language FlatCurry rather than with full Curry suffices, since there exists a type-preserving translation from the latter into the former. In contrast to existing semantics for functional logic languages, we deliberately approach the problem “from the functional side”. That is, rather than adapting approaches previously known from the study of (resolution-like) semantics for logic languages, we aim for a semantics in the spirit of standard denotational semantics for the polymorphic lambda calculus. We claim and set out to prove that the presented semantics is adequate with respect to an existing operational semantics. A particularly interesting aspect, we think, is that we give the first denotational treatment of recursive let-bindings in combination with call-time choice.

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

Buying options

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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S., Jung, A.: Domain theory. In: Handbook of Logic in Computer Science, pp. 1–168. Oxford University Press, Oxford (1994)

    Google Scholar 

  2. Albert, E., Hanus, M., Huch, F., Oliver, J., Vidal, G.: Operational semantics for declarative multi-paradigm languages. Journal of Symbolic Computation 40(1), 795–829 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  3. Braßel, B., Huch, F.: On a tighter integration of functional and logic programming. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 122–138. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Braßel, B., Fischer, S., Hanus, M., Reck, F.: Transforming functional logic programs into monadic functional programs. In: Mariño, J. (ed.) WFLP 2010. LNCS, vol. 6559, pp. 31–48. Springer, Heidelberg (2011)

    Google Scholar 

  5. Christiansen, J., Seidel, D., Voigtländer, J.: Free theorems for functional logic programs. In: Filliâtre, J.-C., Flanagan, C. (eds.) PLPV 2010, pp. 39–48. ACM Press, New York (2010)

    Google Scholar 

  6. Erkök, L.: Value Recursion in Monadic Computations. PhD thesis, OGI School of Science and Engineering, OHSU (2002)

    Google Scholar 

  7. González-Moreno, J.C., Hortalá-González, M.T., López-Fraguas, F.J., Rodríguez-Artalejo, M.: An approach to declarative programming based on a rewriting logic. Journal of Logic Programming 40(1), 47–87 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  8. López-Fraguas, F.J., Rodríguez-Hortalá, J., Sánchez-Hernández, J.: Equivalence of two formal semantics for functional logic programs. In: Lucio, P., Orejas, F. (eds.) PROLE 2006. ENTCS, vol. 188, pp. 117–142. Elsevier, Amsterdam (2007)

    Google Scholar 

  9. López-Fraguas, F.J., Rodríguez-Hortalá, J., Sánchez-Hernández, J.: A fully abstract semantics for constructor systems. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 320–334. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Molina-Bravo, J.M., Pimentel, E.: Composing programs in a rewriting logic for declarative programming. Journal of Theory and Practice of Logic Programming 3(2), 189–221 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  11. Søndergaard, H., Sestoft, P.: Non-determinism in functional languages. The Computer Journal 35(5), 514–523 (1992)

    Article  MathSciNet  Google Scholar 

  12. Wadler, P.: Theorems for free! In: FPCA 1989, pp. 347–359. ACM Press, New York (1989)

    Google Scholar 

  13. Walicki, M., Meldal, S.: Algebraic approaches to nondeterminism: An overview. ACM Computing Surveys 29(1), 30–81 (1997)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Christiansen, J., Seidel, D., Voigtländer, J. (2011). An Adequate, Denotational, Functional-Style Semantics for Typed FlatCurry. In: Mariño, J. (eds) Functional and Constraint Logic Programming. WFLP 2010. Lecture Notes in Computer Science, vol 6559. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20775-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20775-4_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20774-7

  • Online ISBN: 978-3-642-20775-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics