19 JUNHO / TERÇA FEIRA / 03:48
 FCUP PT EN

 APRESENTAÇÃO PESSOAS ENSINO INVESTIGAÇÃO BIBLIOTECA NOTÍCIAS CONTACTOS

### Sabine Broda and Luís Damas

DCC-FC & LIACC, Universidade do Porto
R. do Campo Alegre 823, 4150-180 Porto, Portugal
Phone: 351 22 6078830, Fax: 351 22 6003654
E-mail: {sbb,luis}@ncc.up.pt
January 2004

## Abstract

We define an alternative representation for types in the simply typed $\lambda$-calculus or equivalently for formulas in the implicational fragment of intuitionist propositional logic, which gives us a better insight on the nature of a types structure and its relation to the structure of the set of its normal inhabitants. Based on this representation of a type $\varphi$, called its formula-tree, we define the notion of a valid proof-tree. Any such valid proof-tree represents a finite set of normal inhabitants of $\varphi$ and every normal inhabitant corresponds to exactly one valid proof-tree, constructable with the primitive parts in the formula-tree of $\varphi$. Precise algorithms are given to establish this relation. This method can be used to easily recognize and prove results concerning inhabitation/provability.

FCUP 2018