Technical reports

Subtyping in Ponder
(preliminary report)

Valeria C.V. de Paiva

August 1990, 35 pages

DOI: 10.48456/tr-203

Abstract

This note starts the formal study of the type system of the functional language Ponder. Some of the problems of proving soundness and completeness are discussed and some preliminary results, about fragments of the type system, shown.

It consists of 6 sections. In section 1 we review briefly Ponder’s syntax and describe its typing system. In section 2 we consider a very restricted fragment of the language for which we can prove soundness of the type inference mechanism, but not completeness. Section 3 describes possible models of this fragment and some related work. Section 4 describes the type-inference algorithm for a larger fragment of Ponder and in section 5 we come up against some problematic examples. Section 6 is a summary of further work.

Full text

PDF (1.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-203,
  author =	 {de Paiva, Valeria C.V.},
  title = 	 {{Subtyping in Ponder (preliminary report)}},
  year = 	 1990,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-203.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-203},
  number = 	 {UCAM-CL-TR-203}
}