Author: Johan Georg Granström
Title: Polymorphism in type theory
Abstract: 
A notion of implicit arguments is introduced. The resulting theory
is a conservative extension of Martin-Löf's monomorphic type
theory, with decidable type checking; and it allows for more
implicit arguments than a corresponding notion used in the calculus
of constructions. The conservativity of this extension is related to
Salvesens result that the 1984 version of polymorphic type theory is
not conservative over the monomorphic version.