Subset Types and Partial Functions

摘要

A classical higher-order logic PF_(sub) of partial function is defined. The logic extends a version of Farmer's logic PF by enriching the type system of the logic with subset types and dependent types. Validity in PF_(sub) is then reduced to validity in PF by a translation.