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

  • (no subject)

    noms is a project apparently influenced by camlistore and git. Has a bunch of juicy buzzwords attached to it (Content-addressable, monotonic,…

  • (no subject)

    Great list of computer books from days of yore, with pictures: http://tedfelix.com/books/ I remember "BASIC Fun: Computer Games, Puzzles, and…

  • (no subject)

    One of two large (~$X00) purchases arrived today: a new desktop, since my five-year-old one is starting to show signs of dying. I already pulled all…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded