Aya 证明器，定理证明器和编程语言的结合, 拥有表达力强大的类型系统。
基本信息
- 语言名称：Aya 证明器
- 英文名称：Aya Prover (Aya)
- 语言简介：定理证明器和编程语言的结合, 拥有表达力强大的类型系统, 在类型和值上使用同一个表达式语言
- 相关人员：创始人、核心开发人员 @ice1000
- 语言详述：在语言特性上站在学术界前沿, 同时也是为了实际的使用而设计. 支持高阶归纳类型和交错互归纳互递归, 以及一种全新的类型类机制. 目前较为复杂的特性仍在开发当中. 关于后端, Aya 计划使用双层 JIT 编译, 暂时只开发基于 JVM 的后端.
相关链接
- 官网地址：https://www.aya-prover.org/
- 仓库地址：https://github.com/aya-prover/aya-dev
- 文档地址：So you know some Haskell | Aya Prover 这篇文章暂时介绍了一些目前已经稳定的语言特性, 暂时还在考虑/调整中的语言特性还没有写文档