Realizability for Monotone and Clausular (Co)inductive Definitions

We develop an extension of second order logic (AF2) with monotone, and not only positive, (co)inductive definitions and a clausular feature which simplifies considerably the defining mechanism. A sound realizability interpretation, where the extracted programs are untyped, but typable, terms of a strongly normalizing Curry-style system of monotone (co)inductive types makes our logic into a logical framework suitable for programming with proofs.