2020-09-09 15:17:29 (GMT)
Hello everyone,
@Jasmin Blanchette and I are working on a paper that describes the formalization of the Saturation Framework, including its instantiation of the RP prover of Bachmair and Ganzinger.
Verifying Saturation Provers Modularly
Sophie Tourret and Jasmin Blanchette.
https://matryoshka-project.github.io/pubs/saturate_cpp_draft.pdf
It will be submitted at CPP (deadline 22/09). We would be thankful for any feedback before or after the deadline!
Best
2020-09-11 13:30:2 (GMT)
There's a lot of locales in this paper. I have nothing else to add :sweat_smile:
2020-09-13 21:4:51 (GMT)
If the paper is accepted, we can extend it to 14 pages. Should we add more "content" (as opposed to locale decls)?
2020-09-14 7:9:14 (GMT)
Let's discuss about this when you are back from your vacations. We have a lot of time before the camera-ready version needs to be delivered (and that's only if we get the paper accepted ;-) ).
2020-09-15 18:4:48 (GMT)
Sophie, the question is for Simon, not for you. I want to hear more detailed feedback from Simon.
2020-09-15 18:15:32 (GMT)
Then you should use @Simon Robillard to make sure he is aware that you are writing to him. :wink:
2020-09-15 18:17:15 (GMT)
Oups, I think I got the wrong Simon, did you mean @Simon Cruanes rather than @Simon Robillard ? Given the previous comments and the co-authors of the framework, this is ambiguous...
2020-09-15 18:27:32 (GMT)
Ok, I don't know what went through my head until a few minutes ago. Your message clearly answers @Simon Cruanes 's comment. Sorry @Simon Robillard for the useless mentions.
2020-09-15 18:29:23 (GMT)
Absolutely nothing... ^^'
2020-09-15 18:56:58 (GMT)
Truly I have not much to add, the paper is beyond my level of expertise :smile: . That was just a remark on the level of abstraction y'all seem to favor in Isabelle.
2020-09-15 19:44:8 (GMT)
... says the one who wrote zipperposition in Ocaml using monads ...
2020-09-15 19:44:34 (GMT)
Nah, it's all imperative now :stuck_out_tongue:
2020-09-15 19:53:31 (GMT)
Sophie isn't holding any punches. ;)
2020-09-15 19:56:50 (GMT)
That's a pretty friendly punch! Or maybe it's the french version of a punch.
2020-09-15 19:58:32 (GMT)
In Qc, we say "puntch" not "ponche", btw. ;)
2020-09-15 19:58:51 (GMT)
And you dip fries in it? :thinking:
2020-09-15 19:58:53 (GMT)
Big fan of ti-punch here.
2020-09-15 19:59:9 (GMT)
Of course. With vinegar.
2020-09-15 19:59:33 (GMT)
Had poutine tonight, in Berlin, with real cheese curds. :)
2020-09-15 19:59:34 (GMT)
Currently I'm discovering bourbon (albeit very gently.)
2020-09-15 20:43:57 (GMT)
When I look at the practice of our savate group I would rather not receive a french punch. And I will remember to annoy Jasmin about this poutine source in Berlin.
2020-09-15 20:44:57 (GMT)
Jasmin is like the guy in movies who always knows a bar nearby. Except it's a poutine place.
2020-09-15 20:43:57 (GMT)
When I look at the practice of our savate group I would rather not receive a french punch. And I will remember to annoy Jasmin about this poutine source in Berlin.
2020-09-15 20:44:57 (GMT)
Jasmin is like the guy in movies who always knows a bar nearby. Except it's a poutine place.
2020-09-15 20:53:11 (GMT)
True fact: When we went to Bangkok, I told my wife I'd surely find a poutine place there. On the day of arrival, during the cab ride from the airport, I caught sight of a sign saying "Moose Bar" and "Poutine".
2020-09-15 20:54:3 (GMT)
We just need to reduce P =?= NP to a Poutine place search problem, and collect the prize.
2020-09-15 20:43:57 (GMT)
When I look at the practice of our savate group I would rather not receive a french punch. And I will remember to annoy Jasmin about this poutine source in Berlin.
2020-09-15 20:44:57 (GMT)
Jasmin is like the guy in movies who always knows a bar nearby. Except it's a poutine place.
2020-09-15 20:53:11 (GMT)
True fact: When we went to Bangkok, I told my wife I'd surely find a poutine place there. On the day of arrival, during the cab ride from the airport, I caught sight of a sign saying "Moose Bar" and "Poutine".
2020-09-15 20:54:3 (GMT)
We just need to reduce P =?= NP to a Poutine place search problem, and collect the prize.