Jason (jcreed) wrote,

I talked today at the LF meeting about the result that substitution terminates and behaves well even when you don't know whether the inputs are well-typed — I thought it seemed undermotivated (I mean, for my part, my perennial fascination with gadgety structural induction metrics sufficed) but then William pointed out that there is a variant way to typecheck spines that drills down to the base type as fast as possible, which would be justified by carrying out substitutions before you know they're type-correct. So maybe my stuff is useful for something.
Tags: work
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded