Rob Dickerson @robd@types.pl
PhD Student at Purdue advised by Ben Delaware. PL, formal methods, verification and synthesis.
I mean... it clearly looks like a sky vagina right? A skygina? To the point it's ridiculous to describe it any other way?
How would you use Hoare logic to verify an API migration did not introduce new behaviors? If the API spec allows multiple implementation choices, you need to reason about relational liveness over nondeterministic executions, but relational Hoare logics don't support this kind of reasoning... until now!
Check out my APLAS talk "RHLE: Modular Deductive Verification of Relational ∀∃ Properties" Monday at 1:30p.
🗣️ Talk abstract: https://conf.researchr.org/details/aplas-2022/aplas-2022-papers/20/RHLE-Modular-Deductive-Verification-of-Relational-Properties
📄 Preprint: https://arxiv.org/pdf/2002.02904.pdf
Local Indiana Politics
Always check the local paper for the one unhinged school board candidate who, when given ample time to compose a single paragraph, decides to go with something like this.
I have lived seeing my work appear "years after the shine has dulled," and I can say it is without question a more discouraging experience than the rejections themselves.
https://sigbed.org/2022/08/22/the-toxic-culture-of-rejection-in-computer-science
At the beginning of this video, the two fencers touch each others' arms to test that the scoring machine is working. It isn't, but everyone is on autopilot and nobody notices. The fencers then fence a full touch, which gets annulled because the machine isn't working. This is a toot about CI.
Did you know the original proof assistants were nothing but swords, axes, and arrows? We've come a long way.
Also some of the attempts to match books from the import are pretty amazing. I'm sure these two books are basically the same thing.
Kid has been into Sonic the Hedgehog lately (b/c new movie), so naturally we broke out the Genesis.
PhD Student at Purdue advised by Ben Delaware. PL, formal methods, verification and synthesis.
