Realizability for Monotone and Clausular (Co)inductive Definitions
Favio E. Miranda-Perea · Electronic Notes in Theoretical Computer Science · 2005
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.