/TAPL

Lambda Calculus Implementation in OCaml.

Primary LanguageOCaml

TAPL

Lambda Calculus Implementation in OCaml（程序语言理论项目汇总）

##Overview（文件结构） ###Untyped lambda calculus (self-untyped)

  • Extend arith with arith with untyped lambda calculus
  • Reference
    • Reference Book: Type and Programming Languages
    • arith: implement Chap3-4, untyped
    • untyped: implement Chap5-7, untyped
    • fulluntyped: implement Chap3-4, 5-7, 11, untyped
  • Implementation
    • 参考arith
    • 根据untyped和fulluntyped中的内容，加入Chap5-7的定义；实现难点：context、shift、substitution (tmmap)
    • 仅支持INTV，和Chap3-4, 5-7中定义的Term、Evaluation、Shift、和Substitution规则
    • 支持x@：将x加入namecontext(use AT(@) to replace SLASH(/))
      • x@ (NameBind) 被解析文件
        image
      • x@ (NameBind) 解析结果
        image

###Simply Typed lambda calculus (self-simply-typed)

  • Definition
    • Project 2: extend arith + untyped lambda calculus with types
    • Types: Bool, Nat, T->T
    • Syntax: add \lambda x:T.t
    • First do type checking, and then remove types and evaluate your program by (arith + untyped lambda calculus)
    • No let statements.
  • Reference
    • Reference Book: Type and Programming Languages
    • simplebool: implement Chap9-10, untyped (Bool, ->)
    • 参考simplebool和fullsimple中的内容，加入Chap8的定义；实现难点：context、shift、substitution、TmAbs (tymap)
    • 不再支持x@；使用x:Bool （:Type）作为bind操作符，即将x:Bool作为VarBind加入context
      • :Type (VarBind) 被解析文件
        image
      • :Type (VarBind) 解析结果
        image

###Simply Typed Lambda Calculus with Record and Subtyping (self-simply-sub)

  • Definition
    • Project 3: extend arith + simply typed lambda calculus with records and subtypes
    • Types: add {l1:T1,l2:T2,...,ln:Tn}, Top
    • Syntax: add {l1=t1,l2=t2,...,ln=tn}
    • Use algorithmic subtyping and typing rules, and do not change the typing rule for if-then-else.
  • Reference
    • Reference Book: Type and Programming Languages
    • 参考rcdsubbot和fullsub中的内容，加入Chap15-16的定义；
    • 实现难点：
      • subtype(func)
      • TmRecord, TyRecord
      • TmProj(PathTerm in syntax.ml/parser.mly)
      • Field(Type)s, NEField(Type)s, Field(Type) in parser.mly

##Change Log ###v3.0.1 (2016/06/13 12:56 +08:00)

  • 实现self-simply-sub主体部分，包括Chap15-16中的定义和规则

###v2.0.2 (2016/05/10 17:08 +08:00)

  • 删除prbindingty in main.ml (duplicated with prbinding)
  • 删除TyBinder in parser.mly 和 TyVarBind in syntax.ml(mli) --> TyBinder和TyVarBind现阶段不用？？

###v2.0.1 (2016/05/06 12:00 +08:00)

  • 实现self-simply-typed主体部分，包括Chap8-10中的定义和规则

###v1.0.2 (2016/04/20 13:00 +08:00)

###v1.0.1 (2016/04/20 05:00 +08:00)

  • 实现self-untyped主体部分，包括Chap3-4, 5-7中的定义的Term、Evaluation、Shift、和Substitution规则