[TYPES] Reduction of Martin-Loef type theory with the logical framework to one without it

[anton setzer]

Dear all,

I am currently writing an article on models of Martin-Loef type theory, 
which will be used
to obtain proof theoretic bounds for strong extensions of it. One 
problem is the logical
framework, of which I have heard there exists a proof of the reduction 
of type theory
with the logical framework to type theory without it. Does anybody have 
a reference for that result?

Thanks

Anton

-- 
-----------------------------------------------------------------------------
Anton Setzer                            Telephone:
Department of Computer Science          (national)        (01792) 513368 
University of Wales Swansea             (international) +44 1792  513368
Singleton Park                          Fax:
Swansea SA2 8PP                         (national)        (01792) 295708
UK                                      (international) +44 1792  295708
                                        
Visiting address:                       Email: a.g.setzer at swan.ac.uk
Faraday Building,                       WWW:
Computer Science Dept.            http://www.cs.swan.ac.uk/~csetzer/ 
2nd floor, room 211.      ------------------------------------------------------------------------------