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

Tactics Tactics summary

Attainable speedup

10^6 Quantifier encodning domain choise

10^4 problem simplication autmatic refomrulation

10^2 phase caching t-progapation

cp-sat

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/imandra-docs/

FP and Logic

  • steele
  • verus
  • verona

vs Dijskstra-floyd-hoare

vcc

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

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

  1. run verbose, get statistics -v 10, conflicts grwo but not new quantifier instantions

  2. (apply simplify). What formula is being solved bad rewrte rule, revert

  3. 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

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.

Tactics

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)

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 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

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/PEPM-2023/9/MATLAB-Coder-Partial-Evaluation-in-Practice

  • 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/en-us/research/uploads/prod/2022/07/trmc.pdf

Friday

## 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

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.