∀

Перша формальна система

УДК 004.4, 004.6, 004.9
УДК 510.21, 510.24, 510.25
УДК 510.6
УДК 519.68

Автор: Максим Сохацький (1980)

Анотація

Формальне середовище виконання, система вищих мов та базові бібліотеки для програмування, доведення теорем і формальної філософії

У роботі розказується про новий формальний підхід до математичної верифікації та спробу автора у цій парадигмі побудувати замкнену уніфіковану систему формальних мов для програмування, математики та філософії. В процесі розробки моделі такої системи автору довелося апробувати частини її імплементації для головних SML-подібних формальних академічних мов, мови Erlang та інших (загалом 7 мов). За 10 років автором було проаналізовані синтаксис та семантика основних мов програмування (більше 50 мов) з різних промислових та академічних доменів, 8 мов з яких були особисто реалізовані автором. В роботі описані 8 мов уніфікованої мовної системи (концептуальна модель) та представлені 2 їх імплементації.

Головним чином, натхнення було почерпнуте з LISP-машин минулого, APL-систем, перших систем доведення теорем таких як AUTOMATH, віртуальних маших паралельної та узгодженої обробки нескінченних процесів, таких як BEAM, та кубічних MLTT-пруверів. Робота буде корисною всім аспірантам чистої та прикладної математики, теоретичної інформатики, а також інженерам цих спеціальностей для розуміння природи обчислень.

Офіційне видання

978-617-8027-23-0 М.Сохацький. Перша формальна система. 2021.

Про автора

Максим Сохацький, доктор філософії КПІ (ЄДРПОУ 02070921), буддистський піп-капелан лінії передачі Лонгчен Нінгтік тибетського буддизму (ЄДРПОУ 38778275). Провідний інженер-програміст ДП «ІНФОТЕХ» (ЄДРПОУ 34239034) у підпорядкуванні МВС України (ЄДРПОУ 00032684). Автор «Депозитів ПриватБанк» та «МІА: Документообіг» побудованих на авторських творах ERP.UNO та N2O.DEV.

Продукти дослідження

     🌐   М.Сохацький. Формалізація математики.

     🌐   М.Сохацький. Енциклопедія мов програмування.

     🌐   М.Сохацький. Інститут формальної математики.

     🌐   М.Сохацький. Одноаксіоматична система верифікації «Хенк».

     🌐   М.Сохацький. Модальна гомотопічна мова математики «Андерс».

     🌐   М.Сохацький. Кубічна бібліотека CCHM.

     🌐   М.Сохацький. SMP/AMP ОС та APL мова реального часу.

     🌐   М.Сохацький. Формальна модель розшарувань Хопфа.

Видавництво «Αξίωσις»

Видавництво спеціалізується на наукових дослідженнях, формальних системах, аксіоматичних системах, програмному забезпеченні, математиці, філософії, літературі, мистецтву. Сайт видавництва — axiosis.top