Logic for Computable Functions: Description of a Machine Implementation.

Robin Milner

Research output: Working paper

Abstract / Description of output

This paper is primarily a user''s manual for LCF, a proof-checking program for a logic of computable functions proposed by Dana Scott in 1969 but unpublished by him. We use the name LCF also for the logic itself, which is presented at the start of the paper. The proof-checking program is designed to allow the user interactively to generate formal proofs about computable functions and functionals over a variety of domains, including those of interest to the computer scientist - for example, integers, lists and computer programs and their semantics. The user''s task is alleviated by two features: a subgoaling facility and a powerful simplification mechanism. Applications include proofs of program correctness and in particular of compiler correctness; these applications are not discussed herein, but are illustrated in the papers referenced in this introduction.
Original languageEnglish
Place of PublicationStanford, CA, USA
PublisherStanford University Press
Publication statusUnpublished - 1972

Fingerprint

Dive into the research topics of 'Logic for Computable Functions: Description of a Machine Implementation.'. Together they form a unique fingerprint.

Cite this