⚡

类型规则生成器Skill typing-rule-generator

类型规则生成器是一个专注于编程语言理论领域的工具，用于辅助设计和生成形式化的类型系统推理规则。它能够根据用户定义的语言语法，自动或半自动地生成符合学术规范的LaTeX推理规则、构建类型推导树、分析规则间的依赖关系，并支持导出到Ott、LNGen等机械化验证工具。该技能专为编程语言设计者、编译器开发者和形式化方法研究人员打造，旨在提升类型系统设计的效率和严谨性。 关键词：编程语言理论，类型系统，形式化方法，推理规则，LaTeX，类型推导，PLT，编译器设计

其他 0 次安装 0 次浏览 更新于 2/25/2026

name: typing-rule-generator description: 为类型系统设计生成和格式化推理规则符号中的类型规则 allowed-tools:

  • Bash
  • Read
  • Write
  • Edit
  • Glob
  • Grep metadata: specialization: 计算机科学 domain: 科学 category: 编程语言理论 phase: 6

类型规则生成器

目的

为使用形式化推理规则符号进行编程语言设计提供生成类型规则的专家指导。

能力

  • LaTeX 推理规则生成
  • 语法导向的规则推导
  • 类型推导树构建
  • 规则依赖分析
  • 导出为 Ott/LNGen 格式
  • 处理子类型和多态性

使用指南

  1. 语法定义：正式定义语言语法
  2. 规则设计：为每个结构设计类型规则
  3. 推导树：构建类型推导示例
  4. 格式化：生成出版质量的规则
  5. 导出：导出到机械化工具

工具/库

  • LaTeX (mathpartir)
  • Ott
  • LNGen
  • PLT Redex