LAURENT

ANALYTICAL TYPE SYSTEM

MLTT

  1. PROP
  2. U0 : U1
  3. FORALL
  4. EXISTS
  5. AND
  6. OR
  7. REAL

SET

  1. SET
  2. EQZ3
  3. \
  4. INTERSECT
  5. CLOSURE
  6. POWER
  7. QUOTIENT

CALC

  1. SEQ
  2. INF
  3. SUP
  4. LIMIT
  5. SUM
  6. UNION
  7. MEASURE
  8. LEBESGUE
  9. BOCHER


.

The doesn't have proper syntax yet, that's said you use it as OCaml framework working in pure AST as you would do in Lisp.

$ git clone \ [email protected]:groupoid/laurent $ opam install z3 $ ocamlfind ocamlc -o laurent \ -package z3 -linkpkg src/laurent.ml

SYNTAX

SEMANTICS


MLTT

(-Formation, Dependent Product). -types represents the way we create the spaces of dependent functions with domain in and codomain in type family over .

(-Formation, Dependent Sum). The dependent sum type is indexed over type in the sense of coproduct or disjoint union, where only one fiber codomain is present in pair.

Bibliography


ANALYSIS

[1]. L.Schwartz. Analyse Mathematique (1967)
[2]. E.Bishop. Foundations of Constructive Analysis (1967)
[3]. D.Bridges. Constructive mathematics: a foundation for computable analysis (1999)
[4]. W.Ziemer, M.Torres. Modern Real Analysis (2017)
[5]. A.Booij. Analysis in Univalent Type Theory (2020)
[6]. Z.Murray. Constructive Real Numbers in the Agda (2023)




Присвячується Володимиру Олександровичу Клименку. Механізована верифікація теорем функціонального аналізу і теорії розподілів Лорана Шварца у власній теорії типів на основі MLTT-72. Повторна магістерська робота.