OWHY(ID:448/owh001)

Strawman early functional language

Dana Scott, Oxford U 1969.
Places
People:
Structures:
References:
  • Scott, Dana; "A Type-Theoretical Alternative to CUCH, ISWIM, OWHY", Oxford U 1969. view details
  • Milner, Robin "Implementation and applications of Scott's logic for computable functions" pp1-6 view details Abstract: The basis for this paper is a logic designed by Dana Scott [1] in 1969 for formalizing arguments about computable functions of higher type. This logic uses typed combinators, and we give a more or less direct translation into typed λ-calculus, which is an easier formalism to use, though not so easy for the metatheory because of the presence of bound variables. We then describe, by example only, a proof-checker program which has been implemented for this logic; the program is fully described in [2]. We relate the induction rule which is central to the logic to two more familiar rules - Recursion Induction and Structural Induction - showing that the former is a theorem of the logic, and that for recursively defined structures the latter is a derived rule of the logic. Finally we show how the syntax and semantics of a simple programming language may be described completely in the logic, and we give an example of a theorem which relates syntactic and semantic properties of programs and which can be stated and proved within the logic.
          in SIGPLAN Notices 7(01) January 1972 [ACM] Proc. ACM Conf. on Proving Assertions about Programs. New Mexico State University, Las Cruces, New Mexico (1972) view details