Well-Going Programs Can Be Typed

Kahrs, Stefan (2003) Well-Going Programs Can Be Typed. In: Typed Lambda Calculi and Applications, Jun 10-12, 2003, Valencia, Spain, . (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL


Our idiomatically objectionable title is a pun on Milner's ``well-typed programs do not go wrong'' --- because we provide a completeness result for type-checking rather than a soundness result. We show that the well-behaved functions of untyped PCF are already expressible in typed PCF: any equivalence class of the partial logical equivalence generated from the flat natural numbers in the model given by PCF's operational semantics is inhabited by a well-typed term.

Item Type: Conference or workshop item (UNSPECIFIED)
Additional information: 6th International Conference on Typed Lambda Calculi and Applications (TLCA 2003) VALENCIA, SPAIN, JUN 10-12, 2003
Uncontrolled keywords: PCF, completeness, full abstraction
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:01
Last Modified: 19 Mar 2009 00:20
Resource URI: https://kar.kent.ac.uk/id/eprint/13967 (The current URI for this page, for reference purposes)
  • Depositors only (login required):