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) 被解析文件
      
    • x@ (NameBind) 解析结果
      

###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) 被解析文件
      
    • :Type (VarBind) 解析结果
      

###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)

• 支持x@：将x加入namecontext

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

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