2 papers
cs.LO2025
Fault-Tolerant Multiparty Session Types with Global Escape Loops
Lukas Bartl, Julian Linne, Kirstin Peters
Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e…
cs.LO2025
Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Lukas Bartl, Jasmin Blanchette, Tobias Nipkow
Metis is an ordered paramodulation prover built into the Isabelle/HOL proof assistant. It attempts to close the current goal using a given list of lemmas. Typically these lemmas ar…