Jason (jcreed) wrote,

POPL is happening. Lots of "how've you been?" etc.

Tony Hoare won an award and gave a talk/interview full of lots of quips.

Neel's giving a talk about functional reactive programming.
FRP is great but... naively it's easy to write programs that violate causality, and which leak space. Well, how do we prevent causality problems? Refine the type language so that stream-tomorrow has a different type from stream-today.

head: SA -> A
tail: SA -> *SA
cons : A -> *SA -> SA
fix : (*A -> A) -> A

Can we do the same thing for space leaks?

const : SN -> SSN = \x . fix y . cons(x, y) is bad but
const : N -> SN = \x . fix y . cons(x, y) is okay!

head: SA -> A
tail: SA -> *SA
cons : ◇ -o A -> *(◇ -o SA) -> SA
fix : !(*!A -> !A) -> !A

So the 'good' const we can write as

const :: !X -> ◇ -o S(!X)
const = fix loop . \x. \tok. let !y = x in cons(tok, y, \v.loop x v)


Derek's talk, "Marriage of Bisimulations and Kripke Logical Relations".

Program equivalence in ML-like languages. Want local reasoning about contextual equivalence, but it's tough.

KLRs have step indexing, "more powerful".

Bisimulation "cleaner" for recursion.

Combine them for interlanguage program equivalence? I.e., compiler correctness. Equivalence of program before and after compilation; even in the face of different compilers compiling different parts of your program. Want also 'vertical' compositionality of proofs of equivalence of many stages of compilation.

KLRs not vertically composable. Bisim's doesn't scale in any obvious way to interlanguage reasoning.

Slogan: Don't just support local reasoning, demand it!

The deal is that two programs are equivalent if there's a "consistent" local set of equality-assumptions about function expressions that closes up to the programs being equivalent. The meat of the definition is what "consistent" means. And furthermore the crux of that seems to be some parametrization over arbitrary global knowledge. "Mendler-style coinduction".
Tags: conference, popl

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded