This summer, University of Iowa PhD students Sage Binder and Shweta Rajiv visited Lisbon, Portugal to attend various portions of the Federated Logic Conference (FLoC'26), held from July 13-29. FLoC'26 combined 10 different conferences at one event.
Sage Binder (advisor Katherine Kosaian) presented his research at The International Conference on Interactive Theorem Proving (ITP 2026) , an annual event that began in 1988 and was a part of this year's FLoC'26. ITP can include subjects like program verification, the formalization of mathematics, and the implementation of formal tools.
Here's our interview with Sage on the highlights of his experience at the conference in Portugal:
Q.) Can you share a little about your research presentation?
"We are interested in building tools that support users of interactive theorem provers, which are tools for formal verification. Formal verification is the practice of using specialized logic software to provide high assurance that a certain claim is true. The claim could be, for instance, an important security property about a program, or a mathematical theorem.
"Interactive theorem provers are a specific class of logic tools which allow a user to interactively construct a proof of a claim, usually with the help of very clever automation. Once the proof is completed, the interactive theorem prover certifies the proof is indeed logically valid with respect to a certain set of logical rules and axioms.
"Our work at ITP this year was on our tool for converting proofs in the proof assistant Isabelle/HOL from one particular format to another.
"Just as in software development where there is good code and bad code, so too are there good proofs and bad proofs. Our work focuses on translating proofs written in a 'procedural' style, which tends to be brittle and difficult-to-read, a more explicit 'structured' style. This is useful especially because procedural, while bad for readability and robustness, are sometimes easier to write since they enable the user (or these days, an LLM) to quickly explore different proof approaches. Our work is interested in enabling the best of both worlds, allowing proofs to be constructed procedurally and immediately translated to a more robust and readable format."
Q. What were the highlights of the conference for you?
"The highlight for me was definitely meeting so many people. I've been to conferences before, but the scale of FLoC is so much greater since it is a gathering of 10 conferences. I got to meet so many researchers in my field whom I'd previously only known by name. It was extremely valuable to be able to learn about other peoples' research interests, as well as plan some future collaborations. I especially enjoyed catching up with some colleagues who used to be in our lab (the Computational Logic Center) at The University of Iowa."
Q. What advice would you give for someone presenting at the next ITP conference?
"In your first set of slides, include all the technical details you think are interesting. Then, take out about 90% of those details, leaving only the key ideas that demonstrate the value of your research without overwhelming the audience with details.
"Most people don't want to follow a talk that crams dozens of technical details into 15 or 20 minutes. Rather, your talk is ultimately an advertisement for your paper, so do your best to convince people that your research is really cool and that they should read your paper if they want to know more."
Q. What was it like visiting Portugal?
"Traveling for conferences is definitely a grad student perk. I enjoyed Portugal a lot. The fish was always amazing, and we got some nice opportunities to walk around the old town."