Top

previous chapter Go Model and Object Oriented Programming

next chapter Color Flipping

Hint

Swipe to navigate through the chapters of this book

2015 | OriginalPaper | Chapter

An Intrinsic Denotational Semantics for a Lazy Functional Language

Read first chapter

Author: Leonardo Rodríguez

Publisher: Springer International Publishing

Published in: Programming Languages

» Get access to the full-text

Abstract

In this paper we present a denotational semantics for a lazy functional language. The semantics is intrinsic in the sense that it defines meaning for typing derivations instead of language expressions. We contrast our semantics with the well-known evaluation rules defined by Sestoft [17] and show that these rules preserve types and meaning.

Please log in to get access to this content

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

inform now

Some Formalizations in Coq. http://cs.famaf.unc.edu.ar/ leorodriguez/compilercorrectness/

The Coq Proof Assistant. http://coq.inria.fr/

Abramsky, S.: The lazy lambda calculus. In: Turner, D. (ed.) Research Topics in Functional Programming, pp. 65–116. Addison-Wesley, Boston (1990)

Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993) MathSciNetCrossRefMATH

Benton, N., Kennedy, A., Varming, C.: Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages (2010), unpublished

Breitner, J.: The correctness of Launchbury’s natural semantics for lazy evaluation. Archive of Formal Proofs (2013)

Hughes, R.J.M.: Super-combinators: a new implementation method for applicative languages. In: Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982, pp. 1–10. ACM, New York (1982)

Jones, P.L.S.: Implementing lazy functional languages on stock hardware: the spineless tagless G-machine. J. Funct. Program. 2(2), 127–202 (1992) CrossRefMATH

Josephs, M.B.: The semantics of lazy functional languages. Theor. Compu. Sci. 68(1), 105–111 (1989) MathSciNetCrossRefMATH

10.

Kieburtz, R.B.: The G-machine: a fast, graph-reduction evaluator. In: Jouannaud, J.P. (ed.) FPLCA 1985. LNCS, vol. 201, pp. 400–413. Springer, Heidelberg (1985) CrossRef

11.

Krivine, J.L.: A call-by-name lambda-calculus machine. High. Order Symbolic Comput. 20(3), 199–207 (2007) MathSciNetCrossRefMATH

12.

Launchbury, J.: A natural semantics for lazy evaluation. In: POPL, pp. 144–154 (1993)

13.

Nakata, K.: Denotational semantics for lazy initialization of letrec: black holes as exceptions rather than divergence. In: 7th Workshop on Fixed Points in Computer Science (2010)

14.

Reynolds, J.C.: The Coherence of Languages with Intersection Types. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 675–700. Springer, Heidelberg (1991) CrossRef

15.

Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, New York (1999) MATH

16.

Reynolds, J.C.: The Meaning of Types - From Intrinsic to Extrinsic Semantics. Technical report RS-00-32, BRICS, December 2000

17.

Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231–264 (1997) MathSciNetCrossRefMATH

Title

An Intrinsic Denotational Semantics for a Lazy Functional Language

Book

Programming Languages

Print ISBN: 978-3-319-24011-4

Electronic ISBN: 978-3-319-24012-1

https://doi.org/10.1007/978-3-319-24012-1

DOI

https://doi.org/10.1007/978-3-319-24012-1_6

Author:

Leonardo Rodríguez

Publisher

Springer International Publishing

Sequence number

Premium Partner

Image Credits