On Extensions of AF2 with Monotone and Clausular (Co)inductive Definitions

This thesis discusses some extensions of second-order logic AF2
with primitive constructors representing least and greatest fixed
points of monotone operators, which allow to define predicates by
induction and coinduction. Though the expressive power of
second-order logic has been well-known for a long time and suffices
to define (co)inductive predicates by means of its (co)induction
principles, it is more user-friendly to have a direct way of
defining predicates inductively. Moreover recent applications in
computer science oblige to consider also coinductive definitions
useful for handling infinite objects, the most prominent example
being the data type of streams or infinite lists. Main features of
our approach are the use clauses in the (co)inductive definition
mechanism, concept which simplifies the syntactic shape of the
predicates, as well as the inclusion of not only (co)iteration but
also primitive (co)recursion principles and in the case of
coinductive definitions an inversion principle. For sake of
generality we consider full monotone, and not only positive
definitions, after all positivity is only used to ensure
monotonicity. Working towards practical use of our systems we give
them realizability interpretations where the systems of realizers
are strongly normalizing extensions of the second-order polymorphic
lambda calculus, system F in Curry-style, with (co)inductive types
corresponding directly to the logical systems via the Curry-Howard
correspondence. Such realizability interpretations are therefore
not reductive: the definition of realizability for a (co)inductive
definition is again a (co)inductive definition. As main application
of realizability we extend the so-called programming-with-proofs
paradigm of Krivine and Parigot to our logics, by means of which a
correct program of the lambda calculus can be extracted from a
proof in the logic.