Skip to content
@groupoid

Groupoïd

Лабораторія «Групоїд Інфініті». Факультет прикладної математики Київського політехнічного інституту імені Ігоря Сікорського.

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

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

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

МонографіяІнститутБібліотека

Pinned Loading

  1. anders anders Public

    🧊 Модальний гомотопічний верифікатор математики

    OCaml 19 2

  2. per.ex per.ex Public

    🧊 Числення індуктивних конструкцій

    Erlang 2

  3. alonzo alonzo Public

    🧊 Типізоване ‏-ג‏‎числення

    OCaml 15 1

  4. henk.ex henk.ex Public

    🧊 Чиста система з всесвітами

    Erlang 144 16

  5. joe joe Public

    🧊 Компілятор ML і віртуальна машина

    OCaml 9 1

  6. groupoid.space groupoid.space Public

    🧊 Інститут формальної математики

    TeX 35 13

Repositories

Showing 10 of 12 repositories
  • .github Public
    groupoid/.github’s past year of commit activity
    0 0 0 0 Updated Sep 6, 2024
  • anders Public

    🧊 Модальний гомотопічний верифікатор математики

    groupoid/anders’s past year of commit activity
    OCaml 19 2 0 1 Updated Aug 5, 2024
  • per.rs Public Forked from iho/minitt
    groupoid/per.rs’s past year of commit activity
    Rust 0 1 0 0 Updated Jul 31, 2024
  • per.ex Public

    🧊 Числення індуктивних конструкцій

    groupoid/per.ex’s past year of commit activity
    Erlang 2 0 0 0 Updated Jul 31, 2024
  • henk.rs Public Forked from iho/automath-68
    groupoid/henk.rs’s past year of commit activity
    Rust 0 1 0 0 Updated Jul 30, 2024
  • henk.ex Public

    🧊 Чиста система з всесвітами

    groupoid/henk.ex’s past year of commit activity
    Erlang 144 16 0 0 Updated Jun 27, 2024
  • joe Public

    🧊 Компілятор ML і віртуальна машина

    groupoid/joe’s past year of commit activity
    OCaml 9 1 0 0 Updated Apr 10, 2024
  • monography Public

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

    groupoid/monography’s past year of commit activity
    TeX 92 13 0 0 Updated Apr 10, 2024
  • groupoid.space Public

    🧊 Інститут формальної математики

    groupoid/groupoid.space’s past year of commit activity
    TeX 35 13 0 0 Updated Mar 31, 2024
  • alonzo Public

    🧊 Типізоване ‏-ג‏‎числення

    groupoid/alonzo’s past year of commit activity
    OCaml 15 1 0 0 Updated Mar 20, 2024

Top languages

Loading…

Most used topics

Loading…