Two new papers

I have a post on typestate that has been languishing while I've been spending a lot of time on CMU's admissions committe, but now that that's over I hopefully will be able to get back to it. But first, two papers:

Logical Approximation for Program Analysis

My paper with Frank Pfenning, Logical Approximation for Program Analysis, has been accepted to HOSC. This paper extends of the work from the PEPM 2009 paper Linear logical approximations [ACM Link] - the acceptance is actually to a HOSC special issue on PEPM 2009. However, this paper also synthesizes a lot of stuff from our LICS 2009 paper Substructural Operational Semantics as Ordered Logic Programming. The point of this journal paper is to provide a story about allowing substructural operational semantics specifications of programming language, written in the style of the LICS 2009 paper/my thesis proposal, to be approximated. The approximation process lets us derive program analyses like control flow and alias analysis in the style of the PEPM 2009 paper.

Anyway: PDF, which I'm still polishing for final submission this weekend.

It occurs to me that I should write some more substructural operational semantics posts on this blog, seeing as that's my thesis topic and all.

Constructive Provability Logic

Since Bernardo and I got the principles of constructive provability logic nailed down, we've done a little more exploring. The most important thing about this paper, relative to the technical report, is that it presents a less restricted version of constructive provability logic (the "de-tethered variant" CPL*); I think this less restricted version is going to be critical to understanding logic programming through the lens of constructive provability logic, which is my ultimate goal for the project. The second new thing about the paper is that we nailed down (with one perplexing exception) which of the "normal" axioms of intuitionistic modal logic do or don't hold.

What does this mean? Well, any classical logician will tell you that, in order to be a modal logic, you have to obey one axiom - the "K" axiom, □(A → B) → □A → □B - and one rule, which is that if you can prove A with no assumptions then you can also prove □A ("necessitation"). And any intuitionistic modal logic worth its salt is going to do the same, so far so good. However, intuitionstic modal logic also has a possibility modality ◇A. In classical logic saying something is possible is the same as saying that it's not necessarily false, so ◇A is defined as ¬□¬A. But in intuitionistic logic we tend to think of possibility as a genuinely different thing, and that's where stuff gets complicated. The two most important proof theories for intuitionistic modal logic are probably Alex Simpson's IK - which describes a whole bunch of intuitionistic modal logics - and Pfenning-Davies S4, which describes S4. Some of the axioms that Simpson claims are fundamental to intuitionistic modal logics, like (◇A → □B) → □(A → B), don't hold in Pfenning-Davies S4; it turns out that particular axiom doesn't hold in constructive provability logic, either.

As we discuss in the paper, it seems like the de-tethered variant, CPL*, lies between Pfenning-Davies S4 and Simpson-style S4 on the "which axioms hold" meter, whereas CPL (the tethered version of constructive provability logic from the tech report) may or may not have the same "normal" axioms as Pfenning-Davies; we are currently stuck on whether the ◇◇A → ◇A holds in CPL - it definitely holds in CPL*, Simpson-style S4, and Pfenning-Davies S4, but we are a bit perplexed by our inability to prove or disprove it in CPL.

Here's the PDF, and here's the bitbucket repository with all our Agda. As a side note, "oh, all these proofs are in Agda so we're not discussing them" makes the whole "omitted due to space" thing feel way, way less sketchy. This is just a submission at this point, so comments are especially welcome!