philzook

9 ms·

91.
by philzook 3y ago
You might find these also interesting - Higher-Order, Data-Parallel Structured Deduction https://arxiv.org/pdf/2211.11573.pdf - Functional Programming with Datalog https://drops.dagstuhl.de/opus/vo
92.
by philzook 3y ago
A more direct link to a list of applications of egraphs is https://egraphs-good.github.io/ Largely optimizing rewrites in compilers/synthesizers/query optimizer and theorem proving applications. The egglog repo is
93.
by philzook 3y ago
That is a previous defunct prototype wildly superseded by the current implementation. I still have a soft spot for the syntax though
94.
by philzook 4y ago
Very interesting. Relatedly, I've been refining simple lightweight ways to use a regular SQL database to execute seminaive datalog queries. Path reachability in a graph is the canonical example. One could use stored functions to implem
95.
by philzook 4y ago
I have seen the benefits of: - Having some kind of concrete output to learning or little micro projects. Organizing and adding to my notes is kind of fun. - Documentation for my future self. Sometimes I do go back to refresh. - Some people
96.
MiniLitelog: Easy Breezy SQLite Datalog(philipzucker.com)
3 points by philzook 4y ago|0 comments
97.
by philzook 4y ago
This is a recent paper I thought was really intriguing using Answer Set Programming for a synthesis problem with some very promising sounding results compared to an SMT based approach. http://www.weaselhat.com/2022/11&#
98.
by philzook 4y ago
Depending on what you mean, I'd say datalog is partially characterized as compared to prolog by it's lack of unification (also it's typically executed bottom up and sometimes considered to not have compound terms). Unificat
99.
by philzook 4y ago
From my perspective its main use case is static program analysis. Dataflow analyses over approximating what values certain variables can take or where certain references can point https://yanniss.github.io/points-to-tutorial
100.
by philzook 4y ago
I agree this would be very useful. There are a number of datalog idioms (demand transformations is a big one for encoding functional programs, adding provenance, inlining relations, doing some light compile time backwards proof search) that
101.
by philzook 4y ago
Ah, that's very interesting. Thank you. `s.add(path(x,z) <= edge(x,y) & path(y,z))` is what I chose as python syntax, but it is clunkier.
102.
by philzook 4y ago
Very cool! I love the sqlite install everywhere model. Could you compare use case with Souffle? https://souffle-lang.github.io/ I'd suggest putting the link to the docs more prominently on the github page Is the "
103.
by philzook 4y ago
The problem is people who are smart enough to use fancy features, but not wise enough to show restraint. The question is do we inhibit the wise to protect us from the unwise? The answer might be yes. I enjoy learning about power features so
104.
by philzook 4y ago
What you're describing sounds to me like higher kinded types, which are of some relationship to GATs (GATs enable a better encoding of higher kinded types as I understand it), but are not GATs. https://docs.rs/higher&#x
105.
by philzook 4y ago
I don't agree. If someone has gotten to the point they think they can write anything about a subject it's kind of interesting. Many, many things are undocumented because they are trivial to some and completely unknown to others. E
106.
by philzook 4y ago
It's not for everyone, but I keep running notes in a special section of my blog, which is hosted on github pages, so it all just stays in sync across multiple computers on a repo. I have found it useful even for myself looking up stuff
107.
Datalite: A Simple Datalog Built Around SQLite(philipzucker.com)
4 points by philzook 4y ago|0 comments
108.
Duckegg: A Datalog / Egraph Implementation Built Around DuckDB(philipzucker.com)
4 points by philzook 4y ago|0 comments
109.
by philzook 4y ago
Ciao is a prolog. It is not a new project (I'm saying this as a good thing), for example the reference paper for the system is from 2012 http://cliplab.org/papers/hermenegildo11:ciao-design-tplp.pd... It is still
110.
by philzook 4y ago
Thanks for the suggestion! I've known we should be submitting our verification problems to smtcomp, but hadn't thought about minizinc challenges Our current model is here https://github.com/draperlaboratory/VI
111.
by philzook 4y ago
A very interesting application of constraint programming is the Unison compiler https://unison-code.github.io/ , which uses constraint models to solve compiler backend problems for llvm. As a simple example, register allocat
112.
by philzook 4y ago
Draper Laboratory | Formal Methods Group | Formal Methods Engineers at all levels | Fulltime | Cambridge, MA | https://careers-draper.icims.com/jobs/search?ss=1&searchKeyw... Our group largely works on research pro
113.
The Almighty Dwarf: A Trojan Horse for PL Research(philipzucker.com)
2 points by philzook 4y ago|0 comments
114.
Embedding E-Graph Rewriting in Constraint Handling Rules(philipzucker.com)
2 points by philzook 4y ago|0 comments
115.
by philzook 5y ago
But who can _prove_ the biggest number https://github.com/codyroux/name-the-biggest-number
116.
Constrained Horn Clauses for Bap (2022)(philipzucker.com)
2 points by philzook 5y ago|0 comments
117.
by philzook 5y ago
I've been collating resources I've found here https://www.philipzucker.com/notes/CS/Concurrency/ The replies to this John Regehr thread were particularly rich with links https://twitter.c
118.
by philzook 5y ago
I'm not so sure most lisps are just a wrapper around untyped lambda calculus. The purely functional bits maybe more or less, but mutation and side effects are an integral part of at least scheme and common lisp.
119.
by philzook 5y ago
I have some links up here, including a video and a google colab notebook https://www.philipzucker.com/z3-rise4fun/ http://colab.research.google.com/github/philzook58/z3_tutori...
120.
by philzook 5y ago
The idea that world can't find a way to financially support Clp and Cbc is deeply disappointing. These are such intensely useful projects.

More ›