Prototype proofs and Genericity in Type Theories

Giuseppe Longo
CNRS and ENS, Paris

Logic has proposed and clarified various forms of circularity.  Among them one may recall: non-well-founded sets, self-application and recursive definitions of functions and types, impredicative definitions.  They may be understood in a unified manner, as "mathematical closure properties" of suitable domains of interpretation.  In Type Theory, an analysis of universal second-order (impredicative) propositions may be developped in terms of "prototype proofs and generic arguments", as a fall out of the Genericity Theorem for Girard's system F (papers downloadable from  http://www.dmi.ens.fr/users/longo).