davdar / maam Goto Github PK
View Code? Open in Web Editor NEWA monadic approach to static analysis following the methodology of AAM
License: BSD 3-Clause "New" or "Revised" License
A monadic approach to static analysis following the methodology of AAM
License: BSD 3-Clause "New" or "Revised" License
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?
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?
In the related work, we should include the discussion from our rebuttal that clarifies the relation to Sergey's PLDI paper.
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).
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."
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.
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...)
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.
What are we going to show for the empirical evaluation? We should pick some set of programs (Scheme, Haskell, etc.) and target that.
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}."
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.
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...
There are lots of proofs that I could include if it's valuable to do so.
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?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.