davdar

• Joined on Feb 14, 2011
Apr 30, 2016
davdar opened issue agda/agda#1955
off-by-one error when reporting instance resolution failure
Apr 25, 2016
davdar opened issue agda/agda#1951
Mixfix binders no longer supported in 'syntax'
Apr 20, 2016
• e7a652d
Mar 30, 2016
• 61b2b53
gitignore
Mar 29, 2016
• 50f78cc
Mar 24, 2016
• 58ba855
final update
Mar 23, 2016
• 70b3b26
Mar 23, 2016
• c7d7675
website update
Mar 22, 2016
• 973bff4
draft
Mar 16, 2016
davdar pushed to master at plum-umd/cgc
• f50c2a1
updated version of the development for submission
Mar 15, 2016

It's definitely weird even for people familiar with monad transformers to see StateT taking a monoid arguments. That's a Galois Transformers specif…

Mar 15, 2016

For the paper, you could rename StateT #f to just StateT and call StateT SomeMonoid something like MergeStateT SomeMonoid or JoinStateT SomeMonoid.…

Mar 14, 2016

yeah, cache was the wrong word

Mar 14, 2016

I see, I think Phil was on the right track with the reader idea. To mondaify DVH's example you need to use local when adding something to the seen …

Mar 14, 2016

in my mind it should be analogous to having a cache ($: exp * env * store -> val), except you track a seen cache (seen$ : exp * env * store -> boo…

Mar 14, 2016

if you make the cache path-sensitive rather than flow-insensitive you might get what you're looking for.

Mar 14, 2016

oh shit no, you need two different monads. ListO vs PowO, event for the current setup.

Mar 14, 2016

whereas currently, you only need one monad stack for both evaluators I think.

Mar 14, 2016

Ah right, the monad needs ListO or PowO to know how to combine things... I guess if you go this route, you're looking at two different monad stacks…

Mar 14, 2016

In fact, I think it makes a nice story this way; since the store is an abstract interface, and it can choose how it stores things (single-vs-set), …

Mar 14, 2016

Yeah you could do this in an analogous way to the way we treat the store. Give an abstract interface to tell, call it output, where output takes a …

Mar 10, 2016

\rho* := e . es is just syntax for (let ((\rho e)) (do es)). You can't imperatively update the environment, you can only supply a new environment t…

Mar 9, 2016

I guess there's two types of implementations for state^: one which maps directly to abstract values, and one which maps to sets of abstract values.…

Mar 9, 2016

Nick, does this mean we don't need join as part of the delta interface anymore?

Mar 9, 2016

Okay, DVH and I just chatted and Nick your design is the intended one. Delta should never be operating over sets of things, and variable lookup sho…

Mar 9, 2016

no, in AAM variable lookup should return a set of values, not branch nondeterministically on each element of the powerset. when you need to elimina…

Mar 9, 2016

let's come to consensus before you make such an invasive change to the design. How does vbl need to change between concrete and abstract values (wh…

Mar 9, 2016
Complete and test memo-fixpoint evaluator/ev-combinator
Mar 9, 2016

Maybe this will help think about it: in this compiled version, the ev fixpoint knot is a compile-time fixpoint for traversing expressions. after ty…

Mar 9, 2016
parameterize store update strategy in delta interface