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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramsky, S., Jung, A.: Domain theory. In: Handbook of Logic in Computer Science, pp. 1–168. Oxford University Press, Oxford (1994)
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)
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)
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)
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)
Erkök, L.: Value Recursion in Monadic Computations. PhD thesis, OGI School of Science and Engineering, OHSU (2002)
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)
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)
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)
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)
Søndergaard, H., Sestoft, P.: Non-determinism in functional languages. The Computer Journal 35(5), 514–523 (1992)
Wadler, P.: Theorems for free! In: FPCA 1989, pp. 347–359. ACM Press, New York (1989)
Walicki, M., Meldal, S.: Algebraic approaches to nondeterminism: An overview. ACM Computing Surveys 29(1), 30–81 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)