Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)
Authors: Manfred Schmidt-Schauss and David Sabel
Paper Information
| Title: | Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report) |
| Authors: | Manfred Schmidt-Schauss and David Sabel |
| Proceedings: | WPTE 2014 VSL Proceedings |
| Editors: | Manfred Schmidt-Schauss, David Sabel, Masahiko Sakai and Yuki Chiba |
| Keywords: | contextual equivalence, polymorphic typing, correct program transformation, call-by-need lambda calculus |
| Abstract: | 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. |
| Pages: | 12 |
| Talk: | Jul 13 15:00 |
| Paper: |  |