Partiality and Recursion in Higher-order Logic

Łukasz Czajka

We present an illative system I_s of classical higher-order logic with subtyping and basic inductive types. The system I_s allows for direct definitions of partial and general recu…