Polymorphic Type Assignment and CPS Conversion

Abstract

Meyer and Wand established that the type of a term in the simply typed lambda-calculus may be related in a straightforward manner to the type of its call-by-value CPS transform. This typing property may be extended to Scheme-like continuation-passing primitives, from which the soundness of these extensions follows. We study the extension of these results to the Damas-Milner polymorphic type assignment system under both the call-by-value and call-by-name interpretations. We obtain CPS transforms for the call-by-value interpretation, provided that the polymorphic let is restricted to values, and for the call-by-name interpretation with no restrictions. We prove that there is no call-by-value CPS transform for the full Damas-Milner language that validates the Meyer-Wand typing property and is equivalent to the standard call-by-value transform up to beta eta-conversion.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 1992
Accession Number
ADA250954

Entities

People

  • Mark Lillibridge
  • Robert Harper

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Calculus
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Conversion
  • Grammars
  • Language
  • Linguistics
  • New Jersey
  • Observation
  • Programming Languages
  • Semantics
  • Standards
  • Test And Evaluation

Readers

  • Calculus or Mathematical Analysis
  • Computational Linguistics
  • Military Engineering.