## Paper: Adequacy for untyped translations of typed λ-calculi (at LICS 1993)

Authors:**Wesley Phoa**

### Abstract

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) ⇒_{β} c_{n}, where ⇒_{N} denotes call-by-name evaluation and c_{n} denotes the nth Church numeral. This paper contains a proof of the converse: if Λ(t) ⇒_{β} c_{n} 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} }