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

anton setzer A.G.Setzer at swansea.ac.uk
Tue May 31 17:09:44 EDT 2005

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?



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.      ------------------------------------------------------------------------------

More information about the Types-list mailing list