Programming Computable Functions - Revision history

Jerryobject: Dates clarify.

2025-04-21T09:12:37Z

Dates clarify.

← Previous revision		Revision as of 09:12, 21 April 2025
Line 10:		Line 10:
	\| released = {{Start date and age\|1977\|12}}		\| released = {{Start date and age\|1977\|12}}
	\| latest release version = Full Abstraction		\| latest release version = Full Abstraction
	\| latest release date = {{Start date and age\|2000}}		\| latest release date = {{Start date and age\|2000\|12\|15\|df=yes}}
	\| typing =		\| typing =
	\| memory management =		\| memory management =
Line 126:		Line 126:
	<ref name="Hyland 2000">{{cite journal		<ref name="Hyland 2000">{{cite journal
	\|last1=Hyland \|first1=J. M. E. \|last2=Ong \|first2=C.-H. L.		\|last1=Hyland \|first1=J. M. E. \|last2=Ong \|first2=C.-H. L.
	\|~~year~~=2000		\|date=15 December 2000
	\|title=On Full Abstraction for PCF		\|title=On Full Abstraction for PCF
	\|journal=Information and Computation		\|journal=Information and Computation
Line 137:		Line 137:
	<ref name="Abramsky 2000">{{cite journal		<ref name="Abramsky 2000">{{cite journal
	\|last1=Abramsky \|first1=S. \|last2=Jagadeesan \|first2=R. \|last3=Malacaria \|first3=P.		\|last1=Abramsky \|first1=S. \|last2=Jagadeesan \|first2=R. \|last3=Malacaria \|first3=P.
	\|~~year~~=2000		\|date=15 December 2000
	\|title=Full Abstraction for PCF		\|title=Full Abstraction for PCF
	\|journal=Information and Computation		\|journal=Information and Computation

Jerryobject: Adds: Template:Infobox programming language, parameters, fills, WP:LINKs. WP:REFerence WP:CITation parameters: update-standardize-conform, add, fill.

2025-04-21T08:58:12Z

Adds: Template:Infobox programming language, parameters, fills, WP:LINKs. WP:REFerence WP:CITation parameters: update-standardize-conform, add, fill.

← Previous revision		Revision as of 08:58, 21 April 2025
Line 1:		Line 1:
	{{Short description\|A typed functional language}}		{{Short description\|A typed functional language}}
			{{Infobox programming language
			\| name = Programming Computable Functions
			\| screenshot = <!-- Filename -->
			\| screenshot caption =
			\| sampleCode =
			\| paradigm = [[Functional programming\|functional]]
			\| family =
			\| designers = [[Dana Scott]],<br/>[[Robin Milner]],<br/>[[Gordon Plotkin]]
			\| released = {{Start date and age\|1977\|12}}
			\| latest release version = Full Abstraction
			\| latest release date = {{Start date and age\|2000}}
			\| typing =
			\| memory management =
			\| scope =
			\| programming language =
			\| discontinued = Yes
			\| platform =
			\| operating system =
			\| license =
			\| file ext =
			\| file format = <!-- or: \| file formats = -->
			\| website = <!-- {{URL\|www.example.com}} -->
			\| implementations =
			\| dialects =
			\| influenced by =
			\| influenced =
			}}
	In [[computer science]], '''Programming Computable Functions''' ('''PCF'''), or '''Programming with Computable Functions''', or '''Programming language for Computable Functions''', is a [[programming language]] which is [[Type system\|typed]] and based on [[functional programming]], introduced by [[Gordon Plotkin]] in 1977,<ref name="Plotkin 1977"/> based on prior unpublished material by [[Dana Scott]].{{Efn\|"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions."{{r\|name=Plotkin 1977}} ''Programming Computable Functions'' is used by {{harv\|Mitchell\|1996}}.}} It can be considered as an extended version of the [[typed lambda calculus]], or a simplified version of modern typed functional languages such as [[ML (programming language)\|ML]] or [[Haskell]].		In [[computer science]], '''Programming Computable Functions''' ('''PCF'''), or '''Programming with Computable Functions''', or '''Programming language for Computable Functions''', is a [[programming language]] which is [[Type system\|typed]] and based on [[functional programming]], introduced by [[Gordon Plotkin]] in 1977,<ref name="Plotkin 1977"/> based on prior unpublished material by [[Dana Scott]].{{Efn\|"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions."{{r\|name=Plotkin 1977}} ''Programming Computable Functions'' is used by {{harv\|Mitchell\|1996}}.}} It can be considered as an extended version of the [[typed lambda calculus]], or a simplified version of modern typed functional languages such as [[ML (programming language)\|ML]] or [[Haskell]].

Line 5:		Line 32:

	==Syntax==		==Syntax==
	The ''~~types~~'' of PCF are inductively defined as		The ''[[data type]]s'' of PCF are inductively defined as
	* '''nat''' is a type		* '''nat''' is a type
	* For types ''σ'' and ''τ'', there is a type ''σ'' → ''τ''		* For types ''σ'' and ''τ'', there is a type ''σ'' → ''τ''
Line 57:		Line 84:
	\|first1=Gordon D.		\|first1=Gordon D.
	\|author1-link=Gordon Plotkin		\|author1-link=Gordon Plotkin
	\|~~year~~=1977		\|date=December 1977
	\|title=LCF considered as a programming language		\|title=LCF considered as a programming language
	\|journal=Theoretical Computer Science		\|journal=Theoretical Computer Science
Line 71:		Line 98:
	\|first1=Robin		\|first1=Robin
	\|author1-link=Robin Milner		\|author1-link=Robin Milner
	\|~~year~~=1977		\|date=February 1977
	\|title=Fully abstract models of typed λ-calculi		\|title=Fully abstract models of typed λ-calculi
	\|journal=Theoretical Computer Science		\|journal=Theoretical Computer Science
	\|volume=4		\|volume=4
			\|issue=1
	\|pages=1–22		\|pages=1–22
	\|doi=10.1016/0304-3975(77)90053-6 \|url=https://www.pure.ed.ac.uk/ws/files/15112912/1_s2.0_0304397577900536_main.pdf		\|doi=10.1016/0304-3975(77)90053-6 \|url=https://www.pure.ed.ac.uk/ws/files/15112912/1_s2.0_0304397577900536_main.pdf

Jerryobject: WP:LEADSENTENCE MOS:BOLDSYNonym: adds, clarify. Small WP:COPYEDITs WP:EoS: clarify, WP:TERSE. WP:LINKs: adds, needless WP:PIPEs > WP:NOPIPEs, update-standardizes, WP:RED delink until article exists. WP:REFerence WP:CITation parameters: respaces, cut whitespace characters to standardize, aid work via small screens, update-standardize-conform, reorders, adds, fills. Adds: MOS:COMMENT, WP:CATEGORY.

2025-04-21T08:14:01Z

WP:LEADSENTENCE MOS:BOLDSYNonym: adds, clarify. Small WP:COPYEDITs WP:EoS: clarify, WP:TERSE. WP:LINKs: adds, needless WP:PIPEs > WP:NOPIPEs, update-standardizes, WP:RED delink until article exists. WP:REFerence WP:CITation parameters: respaces, cut whitespace characters to standardize, aid work via small screens, update-standardize-conform, reorders, adds, fills. Adds: MOS:COMMENT, WP:CATEGORY.

Show changes

Oneequalsequalsone: fix note

2025-02-14T14:36:00Z

fix note

← Previous revision		Revision as of 14:36, 14 February 2025
Line 1:		Line 1:
	{{Short description\|A typed functional language}}		{{Short description\|A typed functional language}}
	In [[computer science]], '''Programming Computable Functions''' (PCF) is a [[type system\|typed]] [[Functional programming\|functional language]] introduced by [[Gordon Plotkin]] in 1977,<ref name="Plotkin 1977" /> based on previous unpublished material by [[Dana Scott]].{{r\|~~group=note\|r=~~"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions."{{r\|name=Plotkin 1977}} ''Programming Computable Functions'' is used by {{harv\|Mitchell\|1996}}. It is also referred to as ''Programming with Computable Functions'' or ''Programming language for Computable Functions''.}} It can be considered to be an extended version of the [[typed lambda calculus]] or a simplified version of modern typed functional languages such as [[ML programming language\|ML]] or [[Haskell (programming language)\|Haskell]].		In [[computer science]], '''Programming Computable Functions''' (PCF) is a [[type system\|typed]] [[Functional programming\|functional language]] introduced by [[Gordon Plotkin]] in 1977,<ref name="Plotkin 1977" /> based on previous unpublished material by [[Dana Scott]].{{Efn\|"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions."{{r\|name=Plotkin 1977}} ''Programming Computable Functions'' is used by {{harv\|Mitchell\|1996}}. It is also referred to as ''Programming with Computable Functions'' or ''Programming language for Computable Functions''.}} It can be considered to be an extended version of the [[typed lambda calculus]] or a simplified version of modern typed functional languages such as [[ML programming language\|ML]] or [[Haskell (programming language)\|Haskell]].

	A [[fully abstract]] model for PCF was first given by [[Robin Milner]].<ref name="Milner 1977" /> However, since Milner's model was essentially based on the syntax of PCF it was considered less than satisfactory.<ref name="Ong 1995" /> The first two fully abstract models not employing syntax were formulated during the 1990s. These models are based on [[game semantics]]<ref name="Hyland 2000" /><ref name="Abramsky 2000" /> and [[Kripke logical relations]].<ref name="O'Hearn 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.<ref name="Loader 2001" />		A [[fully abstract]] model for PCF was first given by [[Robin Milner]].<ref name="Milner 1977" /> However, since Milner's model was essentially based on the syntax of PCF it was considered less than satisfactory.<ref name="Ong 1995" /> The first two fully abstract models not employing syntax were formulated during the 1990s. These models are based on [[game semantics]]<ref name="Hyland 2000" /><ref name="Abramsky 2000" /> and [[Kripke logical relations]].<ref name="O'Hearn 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.<ref name="Loader 2001" />
Line 49:		Line 49:

	== Notes ==		== Notes ==
			{{notelist}}
	<references group=note />

	== References ==		== References ==

Citation bot: Altered archive-url. URLs might have been anonymized. Added publisher. | Use this bot. Report bugs. | Suggested by Dominic3203 | Category:Programming language theory | #UCB_Category 17/21

2024-11-29T12:58:50Z

Altered archive-url. URLs might have been anonymized. Added publisher. | Use this bot. Report bugs. | Suggested by Dominic3203 | Category:Programming language theory | #UCB_Category 17/21

← Previous revision		Revision as of 12:58, 29 November 2024
Line 92:		Line 92:
	\|chapter-url = http://users.comlab.ox.ac.uk/luke.ong/publications/index.html		\|chapter-url = http://users.comlab.ox.ac.uk/luke.ong/publications/index.html
	\|access-date = 2006-01-19		\|access-date = 2006-01-19
	\|archive-url = https://web.archive.org/web/20060107195328/http://users.comlab.ox.ac.uk/luke.ong/publications/index.html#		\|archive-url = https://web.archive.org/web/20060107195328/http://users.comlab.ox.ac.uk/luke.ong/publications/index.html
	\|archive-date = 2006-01-07		\|archive-date = 2006-01-07
	\|url-status = dead		\|url-status = dead
Line 158:		Line 158:
	\| isbn = 9780262133210		\| isbn = 9780262133210
	\| chapter = The Language PCF		\| chapter = The Language PCF
			\| publisher = MIT Press
	\| chapter-url = https://theory.stanford.edu/~jcm/books/fpl-chap2.ps		\| chapter-url = https://theory.stanford.edu/~jcm/books/fpl-chap2.ps
	}}		}}

OAbot: Open access bot: doi added to citation with #oabot.

2023-01-30T08:00:04Z

Open access bot: doi added to citation with #oabot.

← Previous revision		Revision as of 08:00, 30 January 2023
Line 105:		Line 105:
	\| issue = 2		\| issue = 2
	\| doi = 10.1006/inco.2000.2917\|url=https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218		\| doi = 10.1006/inco.2000.2917\|url=https://ora.ox.ac.uk/objects/uuid:63c54392-39f3-46f1-8a68-e6ff0ec90218
			\| doi-access = free
	}}</ref>		}}</ref>
	<ref name="Abramsky 2000">{{cite journal		<ref name="Abramsky 2000">{{cite journal
Line 115:		Line 116:
	\| issue = 2		\| issue = 2
	\| doi = 10.1006/inco.2000.2930\| url = http://qmro.qmul.ac.uk/xmlui/handle/123456789/13604		\| doi = 10.1006/inco.2000.2930\| url = http://qmro.qmul.ac.uk/xmlui/handle/123456789/13604
			\| doi-access = free
	}}</ref>		}}</ref>
	<ref name="O'Hearn 1995">{{cite journal		<ref name="O'Hearn 1995">{{cite journal
Line 125:		Line 127:
	\| issue = 1		\| issue = 1
	\| doi = 10.1006/inco.1995.1103\|url=https://surface.syr.edu/lcsmith_other/3		\| doi = 10.1006/inco.1995.1103\|url=https://surface.syr.edu/lcsmith_other/3
			\| doi-access = free
	}}</ref>		}}</ref>
	<ref name="Loader 2001">{{cite journal		<ref name="Loader 2001">{{cite journal

Lexi.lambda: Convert most general references to inline citations

2022-09-30T21:05:23Z

Convert most general references to inline citations

Show changes

Apanatshka: Added a url to the cited chapter of the Mitchell book

2022-05-24T08:49:22Z

Added a url to the cited chapter of the Mitchell book

@@ Line 88: / Line 88: @@
  | hdl-access = free
  }}
 *{{ cite journal
  | author = Abramsky, S., Jagadeesan, R., and Malacaria, P.

Wint7: Adding local short description: "A typed functional language", overriding Wikidata description "typed functional language" (Shortdesc helper)

2021-11-22T09:18:52Z

Adding local short description: "A typed functional language", overriding Wikidata description "typed functional language" (Shortdesc helper)

← Previous revision		Revision as of 09:18, 22 November 2021
Line 1:		Line 1:
			{{Short description\|A typed functional language}}
	In [[computer science]], '''Programming Computable Functions''' (PCF) is a [[type system\|typed]] [[Functional programming\|functional language]] introduced by [[Gordon Plotkin]] in 1977, based on previous unpublished material by [[Dana Scott]].<ref group=note>"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions" {{harv\|Plotkin\|1977}}. ''Programming Computable Functions'' is used by {{harv\|Mitchell\|1996}}. It is also referred to as ''Programming with Computable Functions'' or ''Programming language for Computable Functions''.</ref> It can be considered to be an extended version of the [[typed lambda calculus]] or a simplified version of modern typed functional languages such as [[ML programming language\|ML]] or [[Haskell (programming language)\|Haskell]].		In [[computer science]], '''Programming Computable Functions''' (PCF) is a [[type system\|typed]] [[Functional programming\|functional language]] introduced by [[Gordon Plotkin]] in 1977, based on previous unpublished material by [[Dana Scott]].<ref group=note>"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions" {{harv\|Plotkin\|1977}}. ''Programming Computable Functions'' is used by {{harv\|Mitchell\|1996}}. It is also referred to as ''Programming with Computable Functions'' or ''Programming language for Computable Functions''.</ref> It can be considered to be an extended version of the [[typed lambda calculus]] or a simplified version of modern typed functional languages such as [[ML programming language\|ML]] or [[Haskell (programming language)\|Haskell]].

OAbot: Open access bot: hdl added to citation with #oabot.

2021-09-13T04:46:11Z

Open access bot: hdl added to citation with #oabot.

← Previous revision		Revision as of 04:46, 13 September 2021
Line 84:		Line 84:
	\| volume = 4		\| volume = 4
	\| doi = 10.1016/0304-3975(77)90053-6\| url = https://www.pure.ed.ac.uk/ws/files/15112912/1_s2.0_0304397577900536_main.pdf		\| doi = 10.1016/0304-3975(77)90053-6\| url = https://www.pure.ed.ac.uk/ws/files/15112912/1_s2.0_0304397577900536_main.pdf
			\| hdl = 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1
			\| hdl-access = free
	}}		}}
	*{{cite book\|first=John C.\|last=Mitchell\|authorlink=John C. Mitchell\|title=Foundations for Programming Languages\|year=1996\|chapter=The Language PCF}}		*{{cite book\|first=John C.\|last=Mitchell\|authorlink=John C. Mitchell\|title=Foundations for Programming Languages\|year=1996\|chapter=The Language PCF}}