s— date: 2023-01-22 layout: post title: “POPL 2023 and Puzzle Hunt 2023” —
POPL 23 was right in my backyard in Boston, which was quite convenient.
I think taking notes on my experiences might be very valuable for me, and also possibly others. If this was a thing many people did, you could see for example how well
Finally met Remy in person and spent a lot of time chatting Max’s ear off.
Did a decent job at doing the hallway track. Met a couple people I know from the internet and papers which is always neat. Got to watch Cody in his element holding court.
10^6 Quantifier encodning domain choise
10^4 problem simplication autmatic refomrulation
10^2 phase caching t-progapation
- stanford pascal verifier
- esc/simplify, tep
- nqthm / acl2
- ehdm / pvs. Enhanced Hierarchical Development Methodology? Never heard of this. Oh it’s an SRI thing. Hmm.
- imandra - acl2 for ocaml. hmm. https://docs.imandra.ai/imandra-docs/
FP and Logic
subtyping + polymorpbism is “rathole”
Encoding scheduling problem
use unintepreted functions for custom scheudling theory
MIP encoding is nasty
- pre-solving - hmm. Meta search. Pre-propagate.
- pre-solving 2 - Is this presolving but interleaved with adding constraints?
- custom propagator
- core. possibly minimal set of unsatisfiable assumptions.
- clause trace
- api log - log of api calls
- smt log - log of api calls as smtlib
- lemma log - output learned lemmas in smtlib format
smt.candidate_models=true levent erkok issue
run verbose, get statistics -v 10, conflicts grwo but not new quantifier instantions
(apply simplify). What formula is being solved bad rewrte rule, revert
clause proof logs solver.proof.log=log.smt2
Ths outputs an smtlib script (?) that follows the proof process. But
infer is not smtlib
mbqi = get model, instantiate quantifierd. Hmm. mbqi in egglog? forall nat, lsklddlksdkl -> dkllksdl. How to deal with?
why not ematcing?
bit-blast :blast-quant pure 1-qbf
(set-option :sat-phase always_false) isnpect results from pre-solve (apply simplify)
sat.phase_caching_on = 80000, sat-thread=4 horrible at xor
egglog goal -> z3 (unsat)… Hmm. That’s not bad.
One subgoal model converts to model All subgoal proofs converts to proof
(set-option :model-partial true)
(and-then simplify propagate-values elim-unconstraied qe-light simplify elim-inconstr reduce-args qe-light)
<F,M> - F is clauses split into redundant and irredundant (learned clauses) <F,M,C> - C is conflict state
CDCL(T) = Dual Proof / Model search
SMT presented as inference rules. Is this useful? The execution trace of the smt solver is the proof in this picture. Once again restating that principle. The proof system just is very abstract machine like. But aren’t many of them? Sequents are rather abstract machine-y. Hmm.
Ackermann Reductions Dynamic ackermannization. Decide when to throw in some booleanization of euf. Could lazily instantiate them during search. Let’s CDCL layer prune relevatn seeming equality reasoning. smt.dack.threshold
EUF - empty theory of first order logic Egraph
Equality as actual enode dependency as light weight proof
I just blathered a bunch about egraphs, but they seemed amused. ATP do have clause printing mode. What would you seek? Try to extract a pleasant set of subgoals that imply the target? Kind of makes sense. That’s the analog of simp.
Pretty interesting. I’d like to know about the internals.
User defined propagators Z3
Better AllSAT Logging of quantifier instantiation
Symmetry in SAT
Blissy and Sauce for symmettry detection in graphs?
- The isabelle tutorial
- Incorrectness logic - Greg said this was good
I really didn’t see much this day? I was discussing? Coffee with Max. Aegraph and destructive egrph rewriting may be related
Semantic transformations framework. Seems interesing
Sam told me this one was really good. https://popl23.sigplan.org/details/PEPM-2023/9/MATLAB-Coder-Partial-Evaluation-in-Practice
- Terms for Efficient Proof Checking and Parsing
- Coq Equality - Tassi
- Nadia synthesis talk
Dinner at Penang again :)
Interesting idea from I had never considered: get a post doc and take another go at academia?
Information theory combined with scott domains stuff. Interesting
Hung with Ben. Met Jacques Carette. That’s neat. Gave pitch about egglog for a sound CAS, Agda category equality proofs?
Had to miss Thursday for a day trip to NASA, which was started as a huge boondoggle because I missed my flight, but ended up being fairly successful I think. Was pretty cranky at the start of the week about report revisions distracting me from POPL.
Tail Recursion Modulo Context – An Equational Approach
## https://popl23.sigplan.org/details/POPL-2023-popl-research-papers/44/When-Less-Is-More-Consequence-Finding-in-a-Weak-Theory-of-Arithmetic LIRA
MSL monadic horn clauses
MSL monadic horn clauses reduce to automata. Can go higher order in some way
What are facts? What is unit resolution? Only reductive? That certainly ought to help termination. Resolution prover that only reduces terms. And keeps backwards and forward chaining separate
Herbrand universe Contextual herbrand universe Minimal model. Turnstile vs arrow. We could have a system with no arrow in some sense.
Internalizing rules through hook or crook does make sense. Does only prodcuing
Higher order foroall in datalog. This might be enough to give me set ids? (forall (elem s1 x ) (elem s2 x)) –> (subset s1 s2). (subset s1 s2) (subset s2 s1) -> union s1 s2 Hmm. That’s not strata. It is the “closed” nature of sets. We need to make sure (elem s1 x) is “done” before we can run this rule. So does that mean I can encode this into asp?
Last weekend we did the MIT puzzle hunt for the 3rd year in a row. A grand tradition. We of course did very poorly.
- Froze my ass off in the Commons for “Street Smarts” looking at placards. I way way underdressed. Physically quite unpleasant at the time, but in hindsight very amusing.
- Apples plus Bananas. I just gave up on this one. The boys were doing some insane prime number numerology for hours.