Technical reports

Observations on a linear PCF (preliminary report)

G.M. Bierman

January 1997, 30 pages

DOI: 10.48456/tr-412

Abstract

This paper considers some theoretical and practical issues concerning the use of linear logic as a logical foundation of functional programming languages such as Haskell and SML. First I give an operational theory for a linear PCF: the (typed) linear λ-calculus extended with booleans, conditional and non-termination. An operational semantics is given which corresponds in a precise way to the process of β-reduction which originates from proof theory. Using this operational semantics I define notions of observational equivalence (sometimes called contextual equivalence). Surprisingly, the linearity of the language forces a reworking of the traditional notion of a context (the details are given in an appendix). A co-inductively defined notion, applicative bi-simularity, is developed and compared with observational equivalence using a variant of Howe’s method. Interestingly the equivalence of these two notions is greatly complicated by the linearity of the language. These equivalences are used to study a call-by-name translation of PCF into linear PCF. It is shown that this translation is adequate but not fully abstract. Finally I show how Landin’s SECD machine can be adpacted to execute linear PCF programs.

Full text

PDF (1.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-412,
  author =	 {Bierman, G.M.},
  title = 	 {{Observations on a linear PCF (preliminary report)}},
  year = 	 1997,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-412.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-412},
  number = 	 {UCAM-CL-TR-412}
}