Universidade do Minho  

           
 
  Autenticação/Login
 
Contacts
Site Map
   
  print
 
back 
Varieties of Polymorphism

Abstract: 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.
 
back 
 
  © 2024 Universidade do Minho  - Legal Terms  - updated by CMAT Símbolo de Acessibilidade na Web D.