Programming language for Computable Functions

Programming language for Computable Functions

The Programming language for Computable Functions, or PCF, is a typed functional language introduced by Gordon Plotkin in 1977. It is based on the Logic of Computable Functions (LCF) by Dana Scott. It can be considered as a simplified version of modern typed functional languages such as ML.

A fully abstract model for PCF was first given by Milner (1977). However, since Milner's model was essentially based on the syntax of PCF it was considered less than satisfactory (Ong, 1995). The first two fully abstract models not employing syntax were formulated during the 1990s. These models are based on game semantics (Hyland and Ong, 2000; Abramsky, Jagadeesan, and Malacaria, 2000) and Kripke logical relations (O'Hearn and Riecke, 1995). For a time it was felt that neither of these models was completely satisfactory, since they were not effectively presentable. However, Ralph Loader demonstrated that no effectively presentable fully abstract model could exist, since the question of program equivalence in the finitary fragment of PCF is not decidable.

External links

* [http://www.cs.bham.ac.uk/~mhe/papers/RNC3.pdf Introduction to RealPCF]
* [http://www.cs.pomona.edu/classes/cs131/Parsers/parsePCF.sml Lexer and Parser for PCF written in SML]

ources

* cite journal
author = Abramsky, S., Jagadeesan, R., and Malacaria, P.
title = Full Abstraction for PCF
journal = Information and Computation
date= 2000
pages = 409–470
volume = 163
issue = 2
doi = 10.1006/inco.2000.2930
* cite journal
author = Hyland, J. M. E. and Ong, C.-H. L.
title = On Full Abstraction for PCF
journal = Information and Computation
date= 2000
pages = 285–408
volume = 163
issue = 2
doi = 10.1006/inco.2000.2917
* cite journal
author = O'Hearn, P. W. and Riecke, J. G
title = Kripke Logical Relations and PCF
journal = Information and Computation
date = 1995
pages = 107–116
volume = 120
issue = 1
doi = 10.1006/inco.1995.1103
* cite journal
author = Loader, R.
title = Finitary PCF is not decidable
journal = Theoretical Computer Science
date= 2001
pages = 341–364
volume = 266
issue = 1-2
doi = 10.1016/S0304-3975(00)00194-8
*cite book
author = Ong, C.-H. L.
year = 1995
title = Handbook of Logic in Computer Science
chapter = Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF
editor = Abramsky, S., Gabbay, D., and Maibau, T. S. E.
pages = 269-356
publisher = Oxford University Press
url = http://users.comlab.ox.ac.uk/luke.ong/publications/index.html
* cite journal
author = Plotkin, G. D.
title = LCF considered as a programming language
journal = Theoretical Computer Science
date= 1977
pages = 223–255
volume = 5
doi = 10.1016/0304-3975(77)90044-5


Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • APL (programming language) — APL Paradigm(s) array, functional, structured, modular Appeared in 1964 Designed by Kenneth E. Iverson Developer Kenneth E. Iverson …   Wikipedia

  • Structured programming — can be seen as a subset or subdiscipline of procedural programming, one of the major programming paradigms. It is most famous for removing or reducing reliance on the GOTO statement.Historically, several different structuring techniques or… …   Wikipedia

  • Typed lambda calculus — A typed lambda calculus is a typed formalism that uses the lambda symbol (lambda) to denote anonymous function abstraction. Typed lambda calculi are foundational programming languages and are the base of typed functional programming languages… …   Wikipedia

  • Gordon Plotkin — Gordon D. Plotkin Born 9 September 1946 (1946 09 09) (age 65) Glasg …   Wikipedia

  • Ontology language — In computer science and artificial intelligence, ontology languages are formal languages used to construct ontologies. They allow the encoding of knowledge about specific domains and often include reasoning rules that support the processing of… …   Wikipedia

  • Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… …   Wikipedia

  • Simulism — [The term in the usage in which it appears here seems to have been coined by [http://www.jansch.nl/tag/simulism/ Ivo Jansch] in September 2006. His [http://www.simulism.org Simulism Wiki] is an exploration of Simulism, which invites contributions …   Wikipedia

  • LCF (theorem prover) — LCF (Logic for Computable Functions) is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. LCF introduced the general purpose programming language ML to allow users to write …   Wikipedia

  • Turing completeness — For the usage of this term in the theory of relative computability by oracle machines, see Turing reduction. In computability theory, a system of data manipulation rules (such as an instruction set, a programming language, or a cellular… …   Wikipedia

  • Turing machine — For the test of artificial intelligence, see Turing test. For the instrumental rock band, see Turing Machine (band). Turing machine(s) Machina Universal Turing machine Alternating Turing machine Quantum Turing machine Read only Turing machine… …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”