davdar / maam Goto Github PK

Head off each section with more prose giving intuition.

Keep the implementer in mind at all times, tell them what they need to understand if they want to use it, and what they don't need to know (what we've done for them).

There are lots of proofs that I could include if it's valuable to do so.

• That my monad transformer is indeed a monad (satisfying monad laws)
  • This isn't so long. it relies on the functor laws for the underlying join-semilattice functor though, so that means more category theory language :(
• That my mappings from (a -> m(b)) to (Sigma -> Sigma) are actually themselves Galois connections.
  • These proofs require alpha and gamma to be homomorphisms between categories, and the proofs are more involved.
• That my monad transformer combinations are ordered path-sensitive <= flow-sensitive <= flow-insensitive. I actually haven't done these proofs yet, but I imagine they're simple (since they reduce to proving ordered-ness for monad transformers piecewise).

I like to use vim folding for latex documents rather than splitting a document into files for each section. It makes searching and jumping around a lot easier, but I rely on my editor (vim) to collapse {-{ and }-} unless I ask it to expand those sections.

I change the default fold tags from {{{,}}} to {-{,}-} because }}} shows up quite a lot in latex documents. Here is the line from my vim file that changes this:

autocmd BufReadPost,BufNewFile *.tex exe "set foldmarker={-{,}-}"

If you guys would rather split sections into new files I'm okay doing that too...

Having a hard time getting this to build/run - a git clone and then a make build doesn't do it. After cabal install'ing LambdaJS, things get closer, but not all the way there. Am I missing something obvious?

I haven't abstracted Kon in the semantics yet. Or rather, I haven't replaced Kon with Kon* (a pointer) and heap allocated continuation frames yet. I'd like input for the cleanest way to do this.

Option 1) Make Kon an Addr and heap-allocate continuations. This means Val will be (Int + Clo + Frame).

Option 2) Make Kon an Addr and split continuations into a separate Kon heap. Val will be (Int + Clo) and KStore will map Addr -> Frame. This state space is more amenable to a pushdown abstract (with separate heaps for values and continuations), but I don't plan on adding pushdown to this.

Ideas?

Currently Addr/Time is introduced after exposing abstract domain. The chronology is currently:

Semantics
-> Concrete Interpreter
-> Expose Abstract Domain (Env = Var -> Val)
-> Expose AAM (Env = Var -> Addr, Store = Addr -> Val)
-> Expose Flow Sensitivities (I need a store in the state space so we can talk about widening)

I can imagine an alternate chronology
-> Concrete Interpreter (Env = Var -> Val)
-> Concrete Interpreter with allocation semantics (Env = Var -> Addr, Store = Addr -> Val)
-> Expose Abstract Domain
-> Expose AAM (doesn't alter state space)
-> Expose Flow Sensitivities (also doesn't alter state space)

In terms of the AAM methodology of "design concrete features and then systematically abstract" the second story might be better. Most important is what is more clear for the reader. Thoughts?

Remove the link to hackage and say "URL removed for anonymity."

The title and section font, and maybe the main body font is set not what the sigplan style sheet sets. Looks like CM. Looks like this is the culprit:

\usepackage{fontspec}
\setmonofont[Scale=0.7]{DejaVu Sans Mono}

Not sure what the right workaround is if we want that mono font, but the paper looks a lot better when that is commented out.

His paper introduces an time stamp feature to AAM for which properties can be proven and re-used. Thus it's relevant to discuss as an instance of re-usable metatheory for static analysis.

In papers, we like to write tick as (tick : \Sigma * Time -> Time).

First, in our setting, we don't really have a \Sigma. We're in a monad, which later will be related to a \Sigma by relating (a -> m b) to (\Sigma -> \Sigma).

Second, tick doesn't really need all of \Sigma, but we give it all of \Sigma to claim the interface is very general and admits lots of interesting tick functions. Although, in practice (that is, the practice of writing papers) we only use the Exp and Kon components of \Sigma in the implementation of tick.

Currently I have (tick : Exp * Kon * Time -> Time). Any objections? If I am going to pull out the parts of \Sigma that matter, are Exp and Kon the right parts?

There is an error in the current example for flow sensitivity, pointed out by one of the reviewers. The fix makes the distinction go away, so we need to figure out how to proceed with the example.

What are we going to show for the empirical evaluation? We should pick some set of programs (Scheme, Haskell, etc.) and target that.

The Liang et al paper cites a TR by Moggi for suggesting monad transformers. Is that the right cite (I took a quick look and he doesn't use that term, which isn't to say the idea isn't there...)

For example, it is common to use Val and \widehat{Val} for concrete and abstract values. When we define Val to be a parameter, it would be nice to have a syntactic convention for this which isn't Val or \widehat{Val}. For example:

"To create an analysis we design \widehat{Val} and prove the galois connection \concrete{Val}\galois{\alpha}{\gamma}\widehat{Val}. The interpreter with \parameter{Val} instantiated to \widehat{Val} will then be a correct abstraction of instantiating \parameter{Val} to \concrete{Val}."

In the related work, we should include the discussion from our rebuttal that clarifies the relation to Sergey's PLDI paper.

1. Control parameters (none present in MAI).
2. Reusable proofs (not reusable in MAI).
3. Stronger notion of language independence.
4. More compositional than MAI.