The PVS folks have plans to allow parameterisation of theories by
other theories in the near future (this year?). This might give you
some of what you might need. I doubt though that it would allow
treatment of theories as types to e.g. allow quantification over
theories in individual formulas.
The theorem proving system I know of with the most well developed
`explicit' theory notion is Mizar. In Mizar one can define types that
are are classes of algebraic structures (e.g. of groups, rings etc).
These structure types are like dependent records; fields of elements
of these types are accessible by name and the types of some fields of
elements can depend on the value of other fields. Definitions of
structure types can inherit from previous definitions, and the system
supports subtyping between structure types. [1]
`Explicit theories' can be defined in type theories which include
sigma types (dependent product types) and type universes; the
constructive type theories used in Nuprl, Coq, Lego and Alf, for
example. This approach in its basic form doesn't yield the convenience
of using inheritance in definitions or give the subtyping properties
that one might desire.
I explored this approach in Nuprl in my thesis [2] and a CADE 94 paper.
Jason Hickey at Cornell is working on this in Nuprl at the moment,
extending the type theory with constructs to better support inheritance
and subtyping. I don't think he has much written up on it at the moment,
but you might try mailing him to check [3].
Peter Aczel at Manchester has his Galois project to formalise and
mechanise Galois theory. He has supervised work in Lego with defining
algebraic classes and with automatic inference of forgetful functors
between algebraic classes which effectively gives one a kind of
subtyping.
I imagine too that some basic work must have been possible at Cambridge
with Mike Gordon's HOL-ST and Larry Paulson's set theory work in Isabelle.
Paul Jackson
Here are references I could easily lay my hands on. I can probably dig up
further ones if you are interested.
[1] http://web.cs.ualberta.ca:80/~piotr/Mizar/
The paper "Some Features of the Mizar Language" by Andrzej Trybulec
has a basic description of Mizar structures, and the paper
"The Lattice of Topolotical Domains" illustrates their use.
There are also 100s of examples in the Mizar library.
[2] See my homepage: http://www.dcs.ed.ac.uk/home/pbj/