?

Log in

No account? Create an account
CCF-1218375 - Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

[ website | composition.al ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

CCF-1218375 [Jul. 26th, 2012|10:59 pm]
Lindsey Kuper
[Tags|]

I have some exciting research news to share: the grant proposal that my advisor and I co-wrote and submitted last December has been funded! Barring unforeseen circumstances, this grant will fund my research from now until 2015 or when I graduate, whichever comes first.1

We received the "we expect to be able to fund your proposal" email back in May, but it's taken until now for all the paperwork that makes the grant official to go through, and I didn't want to jump the gun by saying anything publicly before now. Suffice it to say it's been a rather squirmy two months of frequent email-checking and NSF-website-page-reloading. For me, at least, the stakes were pretty high, but getting this grant means that the second half of grad school is beginning to shape up in the way that I had hoped it would.

The work that we proposed is already underway, and I'm going to be giving a couple of talks about it in the near future, starting with a five-minute lightning talk tomorrow. I've been at the Oregon Programming Languages Summer School for the last two weeks, learning lots of new things2 and hanging out with many wonderful people from my research community, one of whom (hi, Gabriel!) graciously organized several sessions' worth of student talks. I've been practicing a bit today, and as it turns out, five minutes is enough time to say approximately nothing whatsoever, but I'm going to give it a shot anyway. Then, three weeks from now, I'll be visiting the BOOM lab at Berkeley and giving a longer talk -- more on that soon.

Hooray!


  1. The latter, hopefully.
  2. To give you an idea of the information density of the summer school, the 80-sheet (so, 160-page) notebook that I bought on July 16 is now over half filled. It's a good thing that we're almost done, because I've just about reached my limit for absorbing new ideas in a short time.
LinkReply

Comments:
From: simrob
2012-07-27 10:02 pm (UTC)
It's backwards because it's also upside down! Don't worry, you probably are starting to understand logic programming.

The idea is to forget everything you know of what it means to do proof search. Paradigm 1, the familiar paradigm (call it the Proof Construction Paradigm, following Andreoli as we are all so wont to do) is "I have a set of sequents that I'm trying to make proofs of these sequents because if I can prove the thing I'm trying to prove has a derivation." In the Proof Construction Paradigm, positive polarity = Datalog, negative polarity = Prolog.

The other paradigm, Paradigm 2, is "let's keep a database of all the sequents we have derivations for because if we can grow that database until it includes the thing I'm trying to prove I will, obviously, be done." This is what's called Inverse Method Theorem Proving, and before you say "that sounds insanely inefficient" remember that it's basically what Forward Chaining does but played out at the level of sequents, not atomic propositions - and Sean McLaughlin is I think putting the finishing touches on the Best Theorem Prover For Intuitionistic Logic In The World (TM) right now and it's based on inverse method theorem proving.

It was in the context of Inverse Method that Kaustuv and company realized that polarity switching made Prolog/Datalog happen, but if your computational model is the inverse method, not the Proof Construction Paradigm, you're growing your derivation trees from the sky down instead of the ground up and everything is reversed: negative polarity gives you Datalog (straightforwardly, actually!) and positive polarity gives you Prolog (in kind of a weird way). Kaustuv wrote a summary newsletter article about this upside-down view, I recommend it.
(Reply) (Parent) (Thread)
From: simrob
2012-07-27 10:06 pm (UTC)
Wow that was really long BUT I WILL DERAIL ANY CONVERSATION TO TALK ABOUT FOCUSING.

(Also congrats on the awesome funding successes Lindsey!)
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2012-07-28 04:00 am (UTC)
I love lengthy asides on PL topics showing up in my blog comments, and will do all I can to encourage them.

(Thanks!)
(Reply) (Parent) (Thread)
[User Picture]From: zacharyzsparks
2012-07-28 07:11 am (UTC)
Derailing To Talk About Focusing For Dummies
(Reply) (Parent) (Thread)