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