Resumo: Second-order logic comes with quantifiers over formulas/types, and proofs of second-order universally quantified formulas require a strong uniformity in the argument. Calculi with types in such a logic are called polymorphic, and terms of second-order universally quantified types enjoy strong relational properties. Polymorphic lambda-calculus is a famous system with a satisfying established meta-theory. In this overview talk, we will highlight mostly results of other researchers in the interplay of logic, calculus/programming and proofs on a computer, ranging from old results of termination, expressivity, genericity, parametricity to recent ones concerning quantifier elimination and the widening towards quantification over the description of datatypes. We also compare with notions of polymorphism that do not stand for uniformity, but the focus is on how to capture just that. |