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