GenProg.Utils

• • Coq选项
  • 保留的记号
  • Extension for pair
  • Extension for option
  • Real numbers
  • LF and CR strings
  • bool missing
  • nat missing
  • string missing
  • list missing
  • Sequence
  • 基于列表的映射，可用于环境管理等场合

GenProg.GenProg

• 核心功能
  • 数组的维数
  • 数据种类。利用依赖类型实现左值和右值的类型匹配
  • data的语义是值类型
  • 环境：id -> value
  • 表达式（右值）
  • 接收器、左值
  • 访问路径，这是 acc 的语义
  • 命令
  • From Functional to Imperative
• Properties of above operations
• 用户程序
  • C Function