Skip to content

Questions

Jump to bottom
Edward Kmett edited this page Dec 6, 2018 · 1 revision

  • Is there an update monad story?

    • Can I use it to recycle the right hand sides of (<*>)'s in modified contexts
    • A computation would return the set of environment variables read and written

  • How to do garbage collection on environments?

    • Seems to need a deep embedding
    • Is this even relevant with a logict style search

  • Can we use propagators to model constraints?

    • Do we replace unification variables with just having join semilattice?
    • Better all-different constraints via the Hall Marriage problem
    • Using discrimination for things like Mehlhorn & Thiel to get more linear all-diffable things

  • SAT solving

    • Conflict clauses should be able to promoted to be used across worlds so long as the latest clause that contributed a unit propagation or contradiction is consistent across both worlds.

  • Reflection without remorse

    • Can it remove some of the performance difference between triangular and idempotent substitutions?
    • Can it fix up some of the hidden costs of LogicT?

  • How to nicely use typed environments?

    • Vault? wants a nice unique variable supply? concurrent-supply

  • Pointwise products of abstract domains?

  • QIP? What is the Abstract-CDCL analogue for SDCL? Wouldn't QIP and QMIP be necessary to handle things like deriving "cheap" equivalent definitions via funext.

  • Can you use WQOs rather than integer costs or mappings of domains to reals for cost analysis?

  • What can be learned from open QBF solving? https://www.cs.cmu.edu/~wklieber/papers/cp2013-qbf-with-free-vars.pdf

  • How do I get crlibm installed and usable dynamically for if I want to have nice floating point intervals?

  • The polyhedral abstract domain is optimized by maintaining a dynamic partitioning of relational variables. The octagon domain could follow suit.

  • What is an efficient encoding of polyhedral/octagon/etc. abstract domain operations that nevertheless remains functional? Can I abuse transients to allow a mostly in-place update policy between world forks?

  • gappa w/ octagons?

  • http://web.engr.oregonstate.edu/~erwig/HaskellRules/

  • From https://people.eecs.berkeley.edu/~necula/Papers/NelsonOppenCong.pdf,

    • We conclude Section 4 with a curiosity: If the axiomatization of the theory of list structure is altered by specifying the result of CAR and CDR on atoms, the problem of determining the satisfiability of a conjunction becomes NP-complete.

    But with types we don't need to do this!

Clone this wiki locally