We give a presentation of Pure type systems where contexts need not bewell-formed . We show that this presentation is equivalent to the usual one . The main motivation for this presentation was that, when we extend Pure type systemswith computation rules, we want to declare constants before the computation rules that are needed to check the type .

Author(s) : Gilles Dowek

Links : PDF - Abstract

Code :

Keywords : presentation - type - pure - rules - computation -

Leave a Reply

Your email address will not be published. Required fields are marked *