Universidade do Minho  

Mapa do Site
Non-standard reductions in simply typed, higher order and dependent type systems with inductive types

One of the fundamental problems in lambda-calculi with inductive types is the problem of relationship between intensional and extensional equality. It is well known that the attempt to replace all extensional (provable) equalities by conversions leads to the systems with bad properties (no SN, undecidable type-checking etc). Our approach is to replace only some extensional equalities (in connection with some concrete purpose) by conversions, in such a way that SN and CR will hold. For example, we considered reductions corresponding to certain isomorphisms f^{-1}f=id (extensional), or equalities between functions on finite types. In the cases we considered it was possible to show SN and CR. In the talk some new technics that were used to show these properties and the problems arising in different calculi will be discussed.
  © 2024 Universidade do Minho  - Termos Legais  - actualizado por CMAT Símbolo de Acessibilidade na Web D.