Implementation and Applications of Scott's Logic for Computable Functions

Robin Milner

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 &lgr;-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.
Original languageEnglish
Title of host publicationProceedings of ACM conference on Proving assertions about programs
PublisherACM
Pages1-6
Number of pages6
DOIs
Publication statusPublished - 1 Jan 1972

Fingerprint

Dive into the research topics of 'Implementation and Applications of Scott's Logic for Computable Functions'. Together they form a unique fingerprint.

Cite this