****MITA LOGIC SEMINAR; PROF. J- P JOUANNAUD'S TALK and a discussion session**** *******************************************************************************
(The meeting is open to everyone without any preregistration)
Theme "Completion methods, in Logic, algebra and Computer science"
The Knuth-style completion procedure bridges Logic, Algebra and Computation. The aim of this meeting is to discuss the completion issue from the logical, algebraic, computer-scientific, historical and philosophical points of view.
Date/Time Sept 22 Thursday 16:30pm-18:00pm Place: Meeting Room number 1, Basement of North Building (Hita-Kan), Mita Campus of Keio University; 5 minutes walking distance from JR-Tamachi, Subway-Mita or Subway-Akabanebashi. we recommend to you to use the East Gate where you find a security guard to ask the exact direction to the Meeting Room, if it is not clear for you with the campus map on our university's homepage.
Main Speaker: Prof. Jean-Pierre Jouannaud, Professor of l'Ecole polytechnique and of INRIA, (French National Instutute of Computer Science) as well as the Ｓｏｆｔｗａｒｅ Chair of :INRIA- Tsinghua(精華大学) Beijing.
Title: A complete tour of completion methods
After the talk, we plan to have a discussion session on Knuth-Huet completions and some ther completion issues from the historical, mathematical, computer-scientific and philosophical view points.Af
Abstract We shall present a unified view of completion methods in abstract algebras (Knuth and Bendix ; Peterson and Stickel; Huet; Jouannaud and Kirchner; Bachmair Dershowitz and Hsiang; Marché; Jouannaud Liu and Luo) and polynomial rings (Janet, Hironaka, Buchberger, Mora). Indeed, there are two quite different completion methods: Janet's methods, based on maintaining an inter-reduced system as a completion invariant, and all the others, based on reaching an inter-reduced system in the limit. As a result, we derive a new completion algorithm for abstract algebras. We conclude with a set of open problems when using an ill-founded completion order (inspired from Hironaka's local ring computation technique).
Profile of the guest speaker: Jean-Pierre Jouannaud graduated from Ecole Polytechnique de Paris and obtained his doctorate from University Paris 6 in 1978. He was then a professor at the universities of Nancy, Paris-Sud, and at Ecole Polytechnique successively, as well as an invited professor at a number of places, including Stanford Research Institute and Stanford University in US, the University of Barcelona in Spain, Keio University in Japan and National Taiwan University in Taiwan. He is now a visiting chair professor at Tsinghua University in Beijing, China, holding a joint appointment with INRIA, the French research institute in ICT.
His current research interests are at the interplay between deduction rules, rewrite rules, decision procedures and type theory, in the development of proof assistants (in particular, Coq, a leading open source proof assistant), and in their application to the formal proof of systems. He is the head of FORmal Methods for Embedded Systems, a joint project of LIAMA, the french-chinese consortium hosting their collaborative research in ICT of which he is the current french director. He published over 100 papers, among which 10 have over one hundred citations each. He won several awards during his career, including the "Prix Montpetit" of the french "Academie des Sciences" and the price for international scientific collaboration delivered by the "Academie des Sciences" and the National Research Council of Taiwan.
He was on the program committee of a number of major international conferences including LICS (chair in 2011), ICALP, CSL, MFCS, FPLCA, RTA, CADE, etc. He created the International Conference on Rewriting Techniques and Applications, the International Conference on Constraints in Computational Logics which later merged with "Constraints" , the international workshops UNIF and CTRS, and the international conference on Certified Proofs and Programs to be held for the first time in 2011 in Kenting, Taiwan. He has been or is a member of the editorial boards of the Journal of Symbolic Computation, Information and Computation, Constraints, Progress in Theoretical Computer Science, and the International Journal of Softare and Informatics. He has been a member of the scientific council of the European Association for Computer Science Logic and of the European Association for Theoretical Computer Science. He has also been a member of the "Fachbeirat" of the Max Planck Institute for Computer Science, and is now on the scientific visiting committee of Academia Sinica, Taiwan. He chaired the jury of the Goedel prize awarded jointly by the EATCS and ACM-SIGACT in 2010, was a member of the jury of the Goedel prize (2008, 2009, 2010), of the LICS "test of time award" 2010, of the Kleene Price 2010, and of the Ackerman price 2011
ご不明な点がございましたら、[email protected] (論理とオント ロジーオープンリサーチセンター事務局まで、ご連絡ください。 岡田光弘、慶応大
------------------------------- .