Logic of Computable Functions: Difference between revisions

Revision as of 16:42, 25 February 2011

Revision as of 16:53, 25 February 2011

Line 1:

'''Logic of Computable Functions''' is a deductive system for computable functions proposed by [[Dana Scott]] in 1969 in an memorandum unpublished memorandumuntil 1993.<ref>RobinDana MilnerS. (1973)Scott. "[ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/73/332/CSA type-TR-73-332.pdftheoretical Modelsalternative ofto LCF]ISWIM, CUCH, OWHY"</ref>. It inspired:''Theoretical

Computer Science'', '''121''':411–440, 1993. Annotated version of the 1969 manuscript.</ref> It inspired:

* [[Logic for Computable Functions]] (LCF), theorem proving logic by [[Robin Milner]].<ref>Robin Milner (1973). "[ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/73/332/CS-TR-73-332.pdf Models of LCF]"</ref>

* [[Programming Computable Functions]] (PCF), small theoretical programming language by [[Gordon Plotkin]].

* [[Logic forProgramming Computable Functions]] (LCFPCF), theoremsmall provingtheoretical logicprogramming language by [[RobinGordon MilnerPlotkin]].<ref>{{ cite journal

| first = Gordon D.

| last = Plotkin

| authorlink = Gordon Plotkin

| title = LCF considered as a programming language

| journal = Theoretical Computer Science

| year = 1977

| pages = 223–255

| volume = 5

| doi = 10.1016/0304-3975(77)90044-5

| url = http://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf

| ref = harv}}</ref>

== References ==