Intuitive Termination Proofs
Title: Intuitive Termination Proofs
Speaker: Jean-Jacques Levy (INRIA, France and ISCAS) pauillac.inria.fr/~levy
Time: 14:00, 4th June 2014
Venue: __ROOM 337__, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
There exists a wide variety of termination proofs for programs. It starts from standard well-founded orderings for imperative or first-order functional languages to complex semantical methods such as Girard’s “Candidats de Réductibilité” for the higher-order system F or the calculi of constructions. In this talk, we recap some of these methods and try to make an intuitive presentation of them. Part of this work was done with Giulio Manzonetto and presented at Antonino Salibra’s 60th anniversary.