H ?
«
‹
←
→
›
»
Language peer sets for LCF:
United Kingdom↑
United Kingdom/1972↑
Designed 1972 ↑
1970s languages ↑
Third generation↑
High Cold War↑
Genus Symbolic ↑
Symbolic↑
Logical↑
Expression-oriented ↑
Symbolic/1972↑
Logical/1972↑
Expression-oriented/1972↑
Symbolic/United Kingdom↑
Logical/United Kingdom↑
Expression-oriented/United Kingdom↑
LCF(ID:1178/lcf001)
Logic for Computable Functions
alternate simple view
Country: United Kingdom
Designed 1972
Published: 1972
Genus: Symbolic
for 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
LCF |
→
|
Edinburgh LCF | |
Implementation of |
References:
Milner, R., Logic for computable functions, descri (1972) Milner, R., Logic for computable functions, description of a machine implementation Artificial Intelligence Memo No. 169,Stanford University (1972).
Milner, Robin (1972) Milner, Robin "Implementation and applications of Scott's logic for computable functions" pp1-6
Extract:
PURE LCF
in [PAAP 1972] (1972) SIGPLAN Notices 7(01) January 1972 [ACM] Proc. ACM Conf. on Proving Assertions about Programs. New Mexico State University, Las Cruces, New Mexico (1972)
Aiello, L. and Aiello, M., (1974) Aiello, L. and Aiello, M., "Proving Program Correctness in LCF"
in (1974) The Colloquium on Programming, Paris, 9-l I April 1974
Aiello, Luigia Aiello, Mario and Weyhrauch, Richar (1974) Aiello, Luigia Aiello, Mario and Weyhrauch, Richard W. "The semantics of PASCAL in LCF." CS-TR-74-447 Department of Computer Science Stanford University August 1974
Abstract
pdf
in (1974) The Colloquium on Programming, Paris, 9-l I April 1974
Aiello, Luigia and Weyhrauch, Richard W. (1974) Aiello, Luigia and Weyhrauch, Richard W. "LCFsmall: an implementation of LCF." CS-TR-74-446 Department of Computer Science Stanford University, August 1974
Abstract
pdf
in (1974) The Colloquium on Programming, Paris, 9-l I April 1974
Finkel, Raphael A. Taylor, Russell H. Bolles, Robe (1974) Finkel, Raphael A. Taylor, Russell H. Bolles, Robert C. Paul, Richard P. Feldman, Jerome A. "AL, a programming system for automation" Report Number: CS-TR-74-456
Department of Computer Science Stanford University
Abstract
pdf
in (1974) The Colloquium on Programming, Paris, 9-l I April 1974
von Henke, Friedrich W (1975) von Henke, Friedrich W "On the representation of data structures in LCF with applications to program generation." Report Number: CS-TR-75-520 Department of Computer Science Stanford University September 1975
Abstract
pdf
in (1974) The Colloquium on Programming, Paris, 9-l I April 1974
Plotkin, Gordon (1977) Plotkin, Gordon "LCF considered as a programming language"
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Jacek Leszczylowski (1980) Jacek Leszczylowski "An Experiment with Edinburgh LCF", 5th Conference on Automated Deduction, Les Arcs, France, LNCS 87, 1980
Online copy
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Cohn, Avra; Milner, Robin (1982) Cohn, Avra; Milner, Robin "On using Edinburgh LCF to prove the correctness of a parsing algorithm" Technical Report UCAM-CL-TR-20 February 1982
Online copy at UCAM
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Paulson, Larry (1983) Paulson, Larry "Recent developments in LCF: examples of structural induction" January 1983 UCAM-CL-TR-34
Online copy
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Paulson, Larry (1983) Paulson, Larry "Rewriting in Cambridge LCF" UCAM-CL-TR-35 February 1983
Abstract
Online copy
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Paulson, Lawrence (1983) Paulson, Lawrence "Tactics and tacticals in Cambridge LCF" Technical Report UCAM-CL-TR-39 July 1983
Online copy
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Paulson, Lawrence (1983) Paulson, Lawrence "The revised logic PPLAMBDA: A reference manual" UCAM-CL-TR-36 March 1983
Abstract
Online copy
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Paulson, Lawrence (1984) Paulson, Lawrence "Lessons learned from LCF" UCAM-CL-TR-54 August 1984
Online copy
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Paulson, Lawrence (1984) Paulson, Lawrence "Verifying the unification algorithm in LCF" Technical Report UCAM-CL-TR-50 March 1984
Abstract
Online copy
Extract:
Overview of LCF
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Paulson, Lawrence C. (1985) Paulson, Lawrence C. "Interactive theorem proving with Cambridge LCF
A user's manual" UCAM-CL-TR-80 November 1985
Online copy
in Theoret. (1977) Theoret. Comput. Sci., 5(3) December 1977
Paulson, LC (1985) Paulson, LC "Lessons learned from LCF: a survey of natural deduction proofs" pp474-479
Abstract
Online copy
in (1985) The Computer Journal 28(5) 1985
Dan Grossman et al (2002) Dan Grossman et al "Region-based Memory Management in Cyclone"
pdf
in [ACM] (2002) ACM Conference on Programming Language Design and Implementation, Berlin, Germany, June, 2002
Search in:
Google
Google scholar
World Cat
Yahoo
Overture
DBLP
Monash bib
NZ
IEEE 
ACM portal
CiteSeer
CSB
ncstrl
jstor
Bookfinder
|