Logic for Computable Functions: различия между версиями

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску
Интерактивная навигация по истории
[непроверенная версия][непроверенная версия]
← Предыдущая правкаСледующая правка →
Содержимое удалено Содержимое добавлено
ВизуальныйВики-текст
Нет описания правки
Строка 10: Строка 10:
== Влияние ==
== Влияние ==
== Литература ==
== Литература ==
{{Reflist}}
{{Refbegin}}
* {{cite book
| last1 = Gordon
| first1 = Michael J.
| author1link = Michael J. C. Gordon
| last2 = Milner
| first2 = Arthur J.
| last3 = Wadsworth
| first3 = Christopher P.
| date = 1979
| title = Edinburgh LCF: A Mechanised Logic of Computation
| doi = 10.1007/3-540-09724-4
| series = Lecture Notes in Computer Science
| volume = 78
| publisher = Springer |location=Berlin Heidelberg
| isbn = 978-3-540-09724-2 }}
* {{cite book
| last = Gordon
| first = Michael J. C.
| chapter = From LCF to HOL: a short history
| url = http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html
| accessdate = 2007-10-11 |title=Proof, language, and interaction
|pages=169–185
|publisher=MIT Press |location=Cambridge, MA|date=2000
|isbn=0-262-16188-5 }}
* {{cite book
| last1 = Loeckx
| first1 = Jacques
| last2 = Sieber
| first2 = Kurt
| date = 1987
| title = The Foundations of Program Verification
| doi = 10.1007/978-3-322-96753-4
| location =
| edition = 2nd
| publisher = Vieweg+Teubner Verlag
| isbn = 978-3-322-96754-1 }}
* {{cite manual
| author = Milner, Robin
| title = Logic for Computable Functions: description of a machine implementation.
| publisher = Stanford University
| date = May 1972
| url = http://www.dtic.mil/dtic/tr/fulltext/u2/785072.pdf }}
* {{cite book
| last = Milner
| first = Robin
| editor = Bečvář, Jiří
| date = 1979
| title = Mathematical Foundations of Computer Science 1979
| chapter = Lcf: A way of doing proofs with a machine
| pages = 146–159
| doi = 10.1007/3-540-09526-8_11
| series = Lecture Notes in Computer Science
| volume = 74
| publisher = Springer |location=Berlin Heidelberg
| isbn = 978-3-540-09526-2}}
{{Refend}}

== Примечания ==
== Примечания ==
{{Примечания}}
{{Примечания}}

Версия от 04:03, 19 апреля 2020

Logic for Computable Functions (рус. Логика для вычислимых функций), (LCF) - это инструмент для интерактивного автоматического доказательства теорем, разработанный Робином Милнером и его сотрудниками в Стэнфорде и Эдинбурге в начале 1970-х годов на базе одноимённой дедуктивной системы, предложенной Даной Скоттом. В ходе работы над системой LCF был разработан универсальный язык программирования ML. Его применение в системе позволило пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и исключения.

Основная идея

Достоинства

Недостатки

Trusted computing base

Проблемы с эффективностью и сложностью процедур доказательств

Влияние

Литература

Примечания

Источник — https://ru.wikipedia.org/w/index.php?title=Logic_for_Computable_Functions&oldid=106442431