Colloquium Computer Science - Prof. M. Ayala University of Brasilia

Title: Formalizing Termination

Abstract:
This talk will present current research on formalization of
termination for a functional language model that contributes to
the meta-theoretical study of the PVS higher-order logic and their
computational aspects.  Automation of the verification of termination
increases flexibility of deductive systems and compilers, and involves
research challenges that range from proving fundamental theorems
about the pertinence of the model to developing mechanical proofs of
the correspondence of different termination criteria that were developed
for several computational frameworks such as Turing machines and
rewriting systems.