Paper: Adequacy for untyped translations of typed λ-calculi (at LICS 1993)
Authors: Wesley PhoaAbstract
PCF is a simply typed λ-calculus with ground types ι (natural numbers) and ο (Booleans); there are no type variables and ⇒ is the only type constructor. There is a natural way to translate any PCF term t into an untyped λ-expression Λ(t), such that if t is a program, i.e. a closed term of ground type (say integer type) and t ⇒N n̅ then Λ(t) ⇒β cn, where ⇒N denotes call-by-name evaluation and cn denotes the nth Church numeral. This paper contains a proof of the converse: if Λ(t) ⇒β cn then t ⇒N n̅; this tells us that the translation is adequate. The proof is semantic, and uses synthetic domain theory to reduce the question to the original Plotkin/Sazonov adequacy theorem for standard domain models of call-by-name PCF. This argument generalises easily to extensions of PCF which can be translated into the untyped λ-calculus: we illustrate this by proving an analogous result for a `second-order' PCF with type quantification. We also discuss how to extend the result to versions of PCF with recursive types and subtyping
BibTeX
@InProceedings{Phoa-Adequacyforuntypedt, author = {Wesley Phoa}, title = {Adequacy for untyped translations of typed λ-calculi}, booktitle = {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993}, year = 1993, editor = {Moshe Vardi}, month = {June}, pages = {287--295}, location = {Montreal, Canada}, publisher = {IEEE Computer Society Press} }