4 citations · 10 across the 7 of their papers we have counts for
7 papers
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…
Global semantic typing for inductive and coinductive computing
Daniel M Leivant
Inductive and coinductive types are commonly construed as ontological (Church-style) types, denoting canonical data-sets such as natural numbers, lists, and streams. For various pu…
Alternating Turing machines for inductive languages
Daniel M Leivant
We show that alternating Turing machines, with a novel and natural definition of acceptance, accept precisely the inductive (Pi-1-1) languages. Total alternating machines, that eit…
Implicit complexity for coinductive data: a characterization of corecurrence
Daniel Leivant, Ramyaa Ramyaa
We propose a framework for reasoning about programs that manipulate coinductive data as well as inductive data. Our approach is based on using equational programs, which support a…