2026-07-23T05:51:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4583 2024-03-06T10:29:35Z ddc:004 open_access

Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report) Schmidt-Schauß, Manfred Sabel, David functional programming polymorphic typing contextual equivalence semantics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Schmidt-Schauß and David Sabel 2014 Is Part Of OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.WPTE.2014.63 urn:nbn:de:0030-drops-45839 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.63 eng https://creativecommons.org/licenses/by/3.0/legalcode