Institution
Creative Electron (United States)
Recent research
- AI & ComputingOpen access
Verified Software Assumes What Its Arithmetic Requires: An Axiom Census of Four Rocq Developments
A machine-checked proof of a program's correctness is conditional on whatever the development assumes, and for deployed software that condition is the whole point. Four Rocq developments are censused with one source-level instrument: the CompCert verified C compiler, fiat-crypto,...
- AI & ComputingOpen access
A formal library's axiom count is routinely reported as a single number. This paper argues that the number conflates two populations which behave differently and answer different questions, and that the conflation is only visible from outside a single library. Five libraries are...
- AI & ComputingOpen access
A formal library's axiom count is routinely reported as a single number. This paper argues that the number conflates two populations which behave differently and answer different questions, and that the conflation is only visible from outside a single library. Five libraries are...