Jason (jcreed) wrote,

So I was going back over the completeness proofs hunting for bugs, and found myself proving a couple little facts about substitution typing and things. It was kind of irritating at first, but the way it worked out is actually quite cute. The fact that I'm tracking the types of the things being substituted in a substantial way, in the very syntax of substitution means I can't just look up the answer in some book or paper (although if anyone listening knows of any work where [M/x] can have different values depending on the type ascribed to M, do let me know) So... it's a very small result -- it's just showing that one two-rule inference system is equivalent to another, that I can describe typing either by conses or snocs -- but it feels ever so mine, and it's a nice little clean result, and as far as me and mathematical work get along, that's the best feeling I know.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded