Skip to content

KOS-TL/KOS-TypeLogic

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

1 Commit
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

KOS-TypeLogic

本目录仅用于理论研究的探索,与仓库中其他目录(如 src/kos-web/、主仓库的 kos-core/面向工程实现的目标不同:此处不交付生产代码,而是将 KOS-TL 的诸多特性内化为类型论本身,为论文与形式化提供实现基础。

与工程实现的区别

  • 不做三层架构划分:不区分 Core / Kernel / Runtime;状态、事件、轨迹、小步演化等均作为类型论的一阶对象(State、Event(σ,σ')、Trace 等)。
  • 理论内化:Event、Trace、State-indexed 依赖类型、因果同一等作为类型论 primitive,便于陈述与证明元定理(确定性重放、Trace = Proof 等)。

子目录 kos-tl

  • kos-tl/:由主仓库 kos-core 复制并重命名而来,作为类型论实现基础。在此副本上扩展 AST、类型规则与归约,引入 Event/Trace/State 等构造。
  • 构建与运行:cd kos-tl && stack build,可执行文件为 kos-tl

与 Future.md 的对应关系

Future.md 方向 本目录下的探索
① 改变类型论本体:Event / Trace 作为 primitive 在 kos-tl 的 AST 与类型规则中引入 StateEvent σ σ'Trace σ 等。
② 证明新元定理 ROADMAP_THEORY.md 中写出形式化命题与证明草图。
③ 将 small-step 内化到类型系统 将 state transition 作为 type-level judgment、Trace 作为 first-class dependent object。

参考

About

type thoery of ZhiXing Logic

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors