Subset Types and Partial Functions

A classical higher-order logic PFsub of partial functions 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 PFsub is then reduced to validity in PF by a translation.

• Type: Conference
• Year: 2003
• Where: CADE
• Authors: Aaron Stump
• Keywords: Automated Reasoning, CADE 2003, Logic Pf