Document Open Access Logo

Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)

Authors Manfred Schmidt-Schauß, David Sabel

PDF
Thumbnail PDF

File

OASIcs.WPTE.2014.63.pdf
  • Filesize: 0.51 MB
  • 12 pages

Document Identifiers

Author Details

Manfred Schmidt-Schauß
David Sabel

Cite As Get BibTex

Manfred Schmidt-Schauß and David Sabel. Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report). In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 63-74, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/OASIcs.WPTE.2014.63

Abstract

This paper presents a call-by-need polymorphically typed lambda-calculus with letrec, case, constructors and seq. The typing of the calculus is modelled in a system-F style. Contextual equivalence is used as  semantics of expressions. We also define a call-by-name variant without letrec. We adapt several tools and criteria for recognizing correct program transformations to polymorphic typing, in particular an inductive applicative simulation.

Subject Classification

Keywords
  • functional programming
  • polymorphic typing
  • contextual equivalence
  • semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. Abramsky. The lazy lambda calculus. In D. A. Turner, editor, Research Topics in Functional Programming, pages 65-116. Addison-Wesley, 1990. Google Scholar
  2. Z. M. Ariola and J. W. Klop. Lambda calculus with explicit recursion. Inform. and Comput., 139(2):154-233, 1997. Google Scholar
  3. J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. CUP, 1994. Google Scholar
  4. Haskell-community. The Haskell Programming Language, 2014. http://www.haskell.org. Google Scholar
  5. D. Howe. Equality in lazy computation systems. In LICS'89, pages 198-203, 1989. Google Scholar
  6. D. Howe. Proving congruence of bisimulation in functional programming languages. Inform. and Comput., 124(2):103-112, 1996. Google Scholar
  7. J. Launchbury. A natural semantics for lazy evaluation. In POPL'93, pages 144-154. ACM, 1993. Google Scholar
  8. A. K. D. Moran, D. Sands, and M. Carlsson. Erratic fudgets: A semantic theory for an embedded coordination language. Sci. Comput. Program., 46(1-2):99-135, 2003. Google Scholar
  9. S. Peyton Jones. Haskell 98 language and libraries: the Revised Report. CUP, 2003. Google Scholar
  10. B. C. Pierce. Types and Programming Languages. The MIT Press, 2002. Google Scholar
  11. A. M. Pitts. Howe’s method for higher-order languages. In Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge Tracts in Theoretical Computer Science, chapter 5, pages 197-232. CUP, November 2011. (chapter 5). Google Scholar
  12. D. Sabel and M. Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci., 18(03):501-553, 2008. Google Scholar
  13. D. Sabel and M. Schmidt-Schauß. A contextual semantics for Concurrent Haskell with futures. In PPDP'11, pages 101-112, New York, NY, USA, July 2011. ACM. Google Scholar
  14. D. Sabel and M. Schmidt-Schauß. Conservative concurrency in Haskell. In LICS'12, pages 561-570. IEEE, 2012. Google Scholar
  15. D. Sabel, M. Schmidt-Schauß, and F. Harwath. Reasoning about contextual equivalence: From untyped to polymorphically typed calculi. In INFORMATIK 2009 (ATPS'09), volume 154 of LNI, pages 369; 2931-45, 2009. Google Scholar
  16. M. Schmidt-Schauß. Correctness of copy in calculi with letrec. In RTA'08, volume 4533 of LNCS, pages 329-343. Springer, 2007. Google Scholar
  17. M. Schmidt-Schauß, E. Machkasova, and D. Sabel. Extending Abramsky’s lazy lambda calculus: (non)-conservativity of embeddings. In RTA'13, volume 21 of LIPIcs, pages 239-254, Dagstuhl, Germany, 2013. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  18. M. Schmidt-Schauß and D. Sabel. On generic context lemmas for higher-order calculi with sharing. Theoret. Comput. Sci., 411(11-13):1521 - 1541, 2010. Google Scholar
  19. M. Schmidt-Schauß, D. Sabel, and E. Machkasova. Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec. Inf. Process. Lett., 111(14):711-716, 2011. Google Scholar
  20. M. Schmidt-Schauß, D. Sabel, and E. Machkasova. Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq. Frank report 49, Goethe-Universität Frankfurt, 2012. Google Scholar
  21. M. Schmidt-Schauß, M. Schütz, and D. Sabel. Safety of Nöcker’s strictness analysis. J. Funct. Programming, 18(04):503-551, 2008. Google Scholar
  22. J. Voigtländer and P. Johann. Selective strictness and parametricity in structural operational semantics, inequationally. Theor. Comput. Sci, 388(1-3):290-318, 2007. Google Scholar
  23. D. Vytiniotis and S. Peyton Jones. Evidence Normalization in System FC (Invited Talk). In RTA'13, volume 21 of LIPIcs, pages 20-38, Dagstuhl, Germany, 2013. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact