Page 17 - Textos de Matemática Vol. 40

Introduction 5
Some aspects of intuitionistic applicative theories are also studied in Troel- stra and van Dalen [TvD88b].
Theses. Applicative theories and explicit mathematics have proven them- selves as a good area for research carried out on a Master and Doctoral level. Therefore, we can refer to a lot of theses containing detailed investigations of certain aspects in this area, in particular from the Bernese school.
Strahm already provides in his Master thesis [Str92] which deals with theories of the strength of PRA, a lot of the basic technical results about ap- plicative theories. His PhD thesis [Str96a] contains a more comprehensive study of the proof theory of applicative theories, including a theory suitable to charac- terize the polytime computable functions as well as theories with quantification operators. His Habilitation [Str01] consists of two parts, the first one deal- ing with metapredicative systems of explicit mathematics, the second one with applicative theories and complexity.
Theories with extended bar induction were studied in an applicative context by Renardel de Lavalette, form Amsterdam, in his PhD thesis [Ren84].
Glaß, from Mu¨nster, studies in his PhD thesis [Gla93] standard structures of explicit mathematics. He investigates, in particular, the aspect of uniformity in the formulation of type existence axioms in explicit mathematics, which is of special interest from the applicative perspective.
In his PhD thesis [Mar94], Marzetta investigates theories of explicit mathematics of predicative strength. He introduces the concept of universes in explicit mathematics.
In our own Master thesis [Kah92], written in Munich, we use an applicative theory to study the implemented proof system lambda which is based on a partial logic. Our PhD thesis [Kah97a] deals with combinatorial properties of applicative theories, and contains a comprehensive study of a truth theory over applicative theories, called Frege structures.
In the Master thesis of Studer, [Stu97], the W-type of Martin-Lo¨f’s type theory is studied in the framework of explicit mathematics. In his PhD the- sis [Stu01b], explicit mathematics is used to study object-oriented programming. This involves (predicative and impredicative) overloading and it is applied to Featherweight Java.
Probst studies in his Master thesis [Pro99] the principle of dependent choice in explicit mathematics and, later on, in his PhD thesis [Pro05] pseudo- hierarchies in both admissible set theory without foundation and explicit math- ematics.
In the Master thesis of Jansen, [Jan97], ontological aspects of explicit mathematics are studied.
A proof-theoretic investigation of various applicative theories based on a primitive-recursive application operation is given in the Master thesis of Steiner [Ste01].
Predicative polymorphism is studied by Kretz, in his Master thesis [Kre02], in a theory of explicit mathematics.