The computational content of atomic polymorphism

Ferreira, Gilda; Vasconcelos, Vasco T

http://hdl.handle.net/10400.2/9415

Utilize este identificador para referenciar este registo.

Nome:	Descrição:	Tamanho:	Formato:
Fat computational content.pdf		435.86 KB	Adobe PDF	Ver/Abrir

Contacte-nos

Autores

Ferreira, Gilda

Vasconcelos, Vasco T

Resumo(s)

We show that the number-theoretic functions de nable in the atomic polymorphic system (Fat) are exactly the extended polynomials. Two proofs of the above result are presented: one reducing the functions' de n- ability problem in Fat to de nability in the simply typed lambda-calculus and other directly adapting Helmut Schwichtenberg's strategy for de nability in the simply typed lambda-calculus to the atomic polymorphic setting. The uniformity granted in the polymorphic system, when compared with the simply typed lambda-calculus, is emphasized.