4 papers · 1 filter
A foundational characterization of Hoare Logic
Daniel Leivant
We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iffit is provable in standard second-order logic with comprehension restricted to…
A generic imperative language for polynomial time
Daniel Leivant
The ramification method in Implicit Computational Complexity has been associated with functional programming, but adapting it to generic imperative programming is highly desirable,…
A theory of finite structures
Daniel Leivant
We develop a novel formal theory of finite structures, based on a view of finite structures as a fundamental artifact of computing and programming, forming a common platform for co…
Implicit complexity via structure transformation
Daniel Leivant, Jean-Yves Marion
Implicit computational complexity, which aims at characterizing complexity classes by machine-independent means, has traditionally been based, on the one hand, on programs and dedu…