Universidade do Minho  

Site Map
October, 12 - Ralph Matthes (IRIT, Universidade Paul Sabatiér de Tolouse)

For applied logics, consistency is an important concern. Logicians are even more concerned with the possibility of proving unprovability of certain principles. Both can often be deduced from weak normalization of the logic: Every proof figure can be turned into a "normal" one.

Typed rewrite systems may be seen as operationalized logics (the famous Curry-Howard isomorphism for lambda-calculi). "Normal" forms of terms correspond to results of computation. Strong normalization becomes desirable: any sequence of rewrites necessarily comes to an end.

If the type system is rich, type normalization may precede term normalization or even be interleaved with it. In current theorem proving environments such as the Coq system, proving and programming are just two aspects of the very same activity.

Using several examples - from widely known to only published ones - the questions of weak and strong normalization will be illustrated for logical systems and functional programming as well as their integration in theorem provers that use dependent types.
  © 2021 Universidade do Minho  - Legal Terms  - updated by CMAT Símbolo de Acessibilidade na Web D.