3 citations · 10 across the 13 of their papers we have counts for
3 papers · 1 filter
Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens +3
Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annot…
Formal Primal-Dual Algorithm Analysis
Mohammad Abdulaziz, Thomas Ammer, Christoph Madlener
We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example…
A Formal Analysis of Capacity Scaling Algorithms for Minimum-Cost Flows
Mohammad Abdulaziz, Thomas Ammer
We present formalisations of the correctness of executable algorithms to solve minimum-cost flow problems in Isabelle/HOL. Two of the algorithms are based on the technique of scali…