Inhabitation of simple types

Sabine Broda, Luís Damas

JLC


Abstract

In this paper we give a complete, formal definition of the formula-tree proof method, prove its correctness and illustrate its adequateness for research in the area of inhabitation of simple types.