Specifying programs with propositions and with congruences

Title: Specifying programs with propositions and with congruences
Speaker: Gilles Dowek
Time:3：00pm, Tuesday，April 14
Venue: Lecture Room,State Key Lab of Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract:Deduction modulo is an extension of first-order predicate logic where axioms are replaced by a congruence, modulo which deduction is performed. Like first-order predicate logic, Deduction modulo is a framework where many theories can be expressed, in particular predicative arithmetic and impredicative arithmetic,usually called first-order and second-order arithmetic. In this work, we give a presentation of Krivine and Parigot’s Second-order functional arithmetic (FA2) in Deduction modulo. Expressing FA2 in Deduction modulo will shed light on an original aspect of the FA2 approach: the fact that programs are specified, not with propositions, but with congruences.

The bio of the speaker:
Gilles Dowek is a professor in le Laboratoire d’Informatique (LIX) at l’école polytechnique (one of the two most famous universities in France) and at l’INRIA-Saclay-?le de France. He is also a consultant for the National Institute of Aerospace, a lab. of the NASA Langley research center. Professor Dowek’s research interests broadly lie in theoretical and applied computer science. They include the formalization of mathematics (type theory, set theory, etc.), proof processing systems (proof-checking, automated theorem proving,etc.), the design of quantum programming languages and the safety of aerospace systems. He has published two books:《Les métamorphoses du calcul》, Le Pommier 2007 (Grand Prix de Philosophie of the Académie fran?aise), 《Principles of Programming Languages》, Springer 2008 and dozens of papers in various international journals and conferences including Handbook of Automated Reasoning，Information and Computation，The Journal of Symbolic Logic，Comptes rendus à l’Académie des Sciences，Theoretical Computer Science，Mathematical Structures in Computer Science，Journal of Automated Reasoning，Annals of Pure and Applied Logic，Symposium on Theoretical Aspects of Computer Science, Journal of Logic and Computation, The Computer Journal , Typed lambda calculi and applications (TLCA), Rewriting techniques and applications (RTA), Automated Deduction

Also he has been in several program committees or as keynote speaker of various international conferences such as IEEE Symposium on Logic in Computer Science (LICS), Typed lambda calculi and applications ( TLCA ), International Conference on Automated Deduction (CADE) etc. Recent invitations include LICS 2009 (member of program committee), IJCAR (CADE, FroCoS, TABLEAUX, FTP) 2008 (co-chair of program committee)