Jason (jcreed) wrote,
Jason
jcreed

-

I think I actually proved a few substantial lemmas in LF+i
now. Good, good.
It looks as if I might actually get in on a paper about this.
Should read over the revised Canonical Forms et alia paper.
Also Frank gave me something by Gougen that does things
semantically --- I don't really understand it very well yet.
Honestly, I think I would feel better about a syntactic
proof of `structural' things like functionality, and I'm
fairly optimistic about them going through without adding
too much to the system that might fuck up adequacy of algorithmic
equality. Then again, maybe my intuition for these things
isn't very well-fueled by experience...
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 

  • 0 comments