Jason (jcreed) wrote,

Went to the ConCert meeting in the morning. Karl talked about meta-theorem proving in twelf. Good to review such things with real examples.

Reading a Statman-Dowek paper (CMU-CS-92-152, amused me that it's exactly ten years before the big ol' ConCert tech report, down to the same tech report number) on finite completeness for lambda-models. Really good stuff. Also got a copy of the Schmidt-Schauß paper from CADE'03, which is apparently not online anywhere. Lame! But a good paper judging it by its content. There's this lemma showing that, under the right circumstances, two terms always behave the same if you feed them to another term just in case they always behave the same if you contrarily feed another term to each of them. This leads to a lovely corollary that if only you could decide λ-definability for finite models (the Statman-Plotkin conjecture), then higher-order matching would be decidable. Sadly, as pointed out, the hypothesis fails. Thanks a heap, Loader! Well, I guess it's not his fault --- he only proved it does. Since I'm a good Platonist, I guess he can't be held responsible for its falsehood.

Made some burgers for dinner. Then sally called asking if I was hungry. I've had very bad timing lately, eating just before others want to eat.

Watched some "Family Guy" at techstep's house. Man, what a great show.

  • (no subject)

    Didn't sleep well. Long day of work. Dinner with akiva at hanamichi.

  • (no subject)

    K was going to do a thing for her dad's birthday, but scheduling kept slipping and slipping so I guess we're going to try doing it tomorrow instead.

  • (no subject)

    Had a pleasant lunch with paul and gabe back from working-at-facebook times. Discussed the important issues of the day, by which I mean video games…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded