Jason (jcreed) wrote,
Jason
jcreed

Type inference and abstraction for HLF seems to work on the entire set of examples from linear cut elimination and the substructural nominal business that I have coded up so far! This is pretty exciting, as it was a very close call for a while whether the unification problems arising from some of the commutative cases of cut elimination were even solvable in principle.
Tags: work
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments