LCF(ID:1178/lcf001)Logic for Computable Functionsfor Logic of Computable Functions Scott 1970 There are two kinds of base variables and constants in LCF. Those that range over individuals and those that range over truth values. People: Related languages
References: PURE LCF We reserve the name LCF (Logic for Computable Functions) for the computer implementation, and give the name PURE LCF to the translation of Scott's logic into k-calculus terms. LCF is a pollution of PURE LCF only in the sense that it attempts to make the process of generating proofs convenient. 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 in The Colloquium on Programming, Paris, 9-l I April 1974 view details Institution: Stanford University, Department of Computer Science Title: The semantics of PASCAL in LCF. Author: Aiello, Luigia Author: Aiello, Mario Author: Weyhrauch, Richard W. Date: August 1974 Abstract: We define a semantics for the arithmetic part of PASCAL by giving it an interpretation in LCF, a language based on the typed $\lambda$-calculus. Programs are represented in terms of their abstract syntax. We show sample proofs, using LCF, of some general properties of PASCAL and the correctness of some particular programs. A program implementing the McCarthy Airline reservation system is proved correct. pdf in The Colloquium on Programming, Paris, 9-l I April 1974 view details Institution: Stanford University, Department of Computer Science Title: LCFsmall: an implementation of LCF. Author: Aiello, Luigia Author: Weyhrauch, Richard W. Date: August 1974 Abstract: This is a report on a computer program implementing a simplified version of LCF. It is written (with minor exceptions) entirely in pure LISP and has none of the user oriented features of the implementation described by Milner. We attempt to represent directly in code the metamathematical notions necessary to describe LCF. We hope that the code is simple enough and the metamathematics is clear enough so that properties of this particular program (e.g. its correctness) can eventually be proved. The program is reproduced in full. pdf in The Colloquium on Programming, Paris, 9-l I April 1974 view details Institution: Stanford University, Department of Computer Science Title: AL, a programming system for automation. Author: Finkel, Raphael A. Author: Taylor, Russell H. Author: Bolles, Robert C. Author: Paul, Richard P. Author: Feldman, Jerome A. Date: November 1974 Abstract: AL is a high-level programming system for specification of manipulatory tasks such as assembly of an object from parts. AL includes an ALGOL-like source language, a translator for converting programs into runnable code, and a runtime system for controlling manipulators and other devices. The system includes advanced features for describing individual motions of manipulators, for using sensory information, and for describing assembly algorithms in terms of common domain-specific primitives. This document describes the design of AL, which is currently being implemented as a successor to the Stanford WAVE system. in The Colloquium on Programming, Paris, 9-l I April 1974 view details Institution: Stanford University, Department of Computer Science Title: On the representation of data structures in LCF with applications to program generation. Author: von Henke, Friedrich W. Date: September 1975 Abstract: In this paper we discuss techniques of exploiting the obvious relationship between program structure and data structure for program generation. We develop methods of program specification that are derived from a representation of recursive data structures in the Logic for Computable Functions (LCF). As a step towards a formal problem specification language we define definitional extensions of LCF. These include a calculus for (computable) homogeneous sets and restricted quantification. Concepts that are obtained by interpreting data types as algebras are used to derive function definition schemes from an LCF term representing a data structure; they also lead to techniques for the simplification of expressions in the extended language. The specification methods are illustrated with a detailed example. pdf in The Colloquium on Programming, Paris, 9-l I April 1974 view details in Theoret. Comput. Sci., 5(3) December 1977 view details in Theoret. Comput. Sci., 5(3) December 1977 view details in Theoret. Comput. Sci., 5(3) December 1977 view details in Theoret. Comput. Sci., 5(3) December 1977 view details LCF is an interactive theorem-prover intended for reasoning about computation. Its implementation of rewriting is presented in detail. LCF provides a family of rewriting functions, and operators to combine them. A succession of functions is described, from pattern matching primitives to the rewriting tool that performs most inferences in LCF proofs. The design is highly modular. Each function performs a basic, specific task, such as recognizing a certain form of tautology. Each operator implements one method of building a rewriting function from simpler ones. These pieces can be put together in numerous ways, yielding a variety of rewriting strategies. The approach involves programming with higher-order functions. Rewriting functions are data values, produced by computation on other rewriting functions. The code is in daily use at Cambridge, demonstrating the practical use of functional programming. External link: Online copy Internal error SAYFLD: Field name [txtURL] not in current recordsetsaying value... in Theoret. Comput. Sci., 5(3) December 1977 view details in Theoret. Comput. Sci., 5(3) December 1977 view details PPLAMBDA?s rule of fixed-point induction admits a wide class of inductions, particularly where flat or finite types are involved. The user can express and prove these type properties in PPLAMBDA. The induction rule accepts a list of theorems, stating type properties to consider when deciding to admit an induction. External link: Online copy in Theoret. Comput. Sci., 5(3) December 1977 view details in Theoret. Comput. Sci., 5(3) December 1977 view details Overview of LCF LCF is an interactive, programmable theorem prover for Scott's Logic of Computable Functions. There are several versions of LCF. Cohn has used Edinburgh LCF to prove the equivalence of two semantic definitions of a simple programming language [10]. Mulmuley has used it to automate existence proofs for inclusive predicates, a highly technical aspect of compiler verification [20]. Gordon has extended Cambridge LCF for reasoning about hardware, and proved the correctness of a small computer [14]. This section introduces the principles; tutorials have appeared elsewhere [12, 13]. The unification proof uses Cambridge LCF. in Theoret. Comput. Sci., 5(3) December 1977 view details in Theoret. Comput. Sci., 5(3) December 1977 view details There is an extensive bibliography of work related to LCF. The most dynamic issues at present are data types, subgoaling techniques, logics of computation, and the development of ML. External link: Online copy in The Computer Journal 28(5) 1985 view details in ACM Conference on Programming Language Design and Implementation, Berlin, Germany, June, 2002 view details |