Popl 2023
s— date: 20230122 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.
Talks
Monday
Z3 tutorial
Was really excited for the Z3 tutorial, which kind of went by so fast I’m not sure how much of what was being said I caught. internals doc slides
Attainable speedup
10^6 Quantifier encodning domain choise
10^4 problem simplication autmatic refomrulation
10^2 phase caching tprogapation
cpsat
autoactive?
 stanford pascal verifier
 esc/simplify, tep

boogie
 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/imandradocs/
FP and Logic
 steele
 verus
 verona
vs Dijskstrafloydhoare
vcc
subtyping + polymorpbism is “rathole”
Encoding scheduling problem
use unintepreted functions for custom scheudling theory
MIP encoding is nasty
 presolving  hmm. Meta search. Prepropagate.
 presolving 2  Is this presolving but interleaved with adding constraints?
 custom propagator
Case study
Retrieving information
 model
 core. possibly minimal set of unsatisfiable assumptions.
 proof
 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
axiomprofiler
OnClause
tr:modelchecker
mbqi = get model, instantiate quantifierd. Hmm. mbqi in egglog? forall nat, lsklddlksdkl > dkllksdl. How to deal with?
why not ematcing?
trying qsat
bitblast :blastquant pure 1qbf
(setoption :satphase always_false) isnpect results from presolve (apply simplify)
sat.phase_caching_on = 80000, satthread=4 horrible at xor
egglog goal > z3 (unsat)… Hmm. That’s not bad.
Tactics
One subgoal model converts to model All subgoal proofs converts to proof
(setoption :modelpartial true)
(andthen simplify propagatevalues elimunconstraied qelight simplify eliminconstr reduceargs qelight)
Solving Process
<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 machiney. 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
Iterative Deepening
EUF  empty theory of first order logic Egraph
Equality as actual enode dependency as light weight proof
Lunch
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.
SassyLF
Pretty interesting. I’d like to know about the internals.
User defined propagators Z3
Better AllSAT Logging of quantifier instantiation
CosySel
Symmetry in SAT
Blissy and Sauce for symmettry detection in graphs?
Checkout later
 The isabelle tutorial
 Incorrectness logic  Greg said this was good
Tuesday
I really didn’t see much this day? I was discussing? Coffee with Max. Aegraph and destructive egrph rewriting may be related
Incremental Souffle
Aesop
Semantic Rewriting
Semantic transformations framework. Seems interesing
Matlab
Sam told me this one was really good. https://popl23.sigplan.org/details/PEPM2023/9/MATLABCoderPartialEvaluationinPractice
 Terms for Efficient Proof Checking and Parsing
 Coq Equality  Tassi
 Nadia synthesis talk
Wednesday
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
Reception
Hung with Ben. Met Jacques Carette. That’s neat. Gave pitch about egglog for a sound CAS, Agda category equality proofs?
Thursday
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://www.microsoft.com/enus/research/uploads/prod/2022/07/trmc.pdf
Friday
## https://popl23.sigplan.org/details/POPL2023poplresearchpapers/44/WhenLessIsMoreConsequenceFindinginaWeakTheoryofArithmetic LIRA
MSL monadic horn clauses
MSL monadic horn clauses reduce to automata. Can go higher order in some way
Bisimulation Minimization
https://github.com/julesjacobs/boa
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?
Puzzle Hunt
Last weekend we did the MIT puzzle hunt for the 3rd year in a row. A grand tradition. We of course did very poorly.
Some highlights:
 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.
 The cryptic crossword puzzle. It was this insane self referential infinite zoom javascript thing.