**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)