Wednesday, April 22, 2009
Prof. Chuck Liang
Department of Computer Science
Title: A Unified System for the Structured Construction of Proofs
Proof theory is a branch of mathematical logic that seeks to formalize the deductive arguments used by mathematicians as well as the algorithmic process that underlies the execution of computer programs. In fact proof and program are shown to be equivalent notions under certain settings. I will present my recent work on focused proofs, which seek to structure all proofs in a uniform way. In addition, the various "logics" used in theoretical computer science, including classical, intuitionistic and linear logic, can all be seen as fragments of a unified framework. In this way this work can be called "abstract proof theory". The fundamental consistency of various logical systems, captured in a property called cut-elimination, can be given a single, unifying proof in this framework. Focused proofs are based on a notion of duality that is found in both logic and computer science. Forward search versus goal-directed search, asynchronous versus synchronous execution, producer-consumer paradigm, call-by-value versus call-by-name: these are all examples of phenomenon that occur naturally in computer science and which are reflected by choices that can be made in the construction of focused proofs. This work is in collaboration with Dale Miller at Ecole Polytechnique in France. This talk will follow a similar talk I gave last semester, but attendance at the previous talk is not required.
Biography:Prof. Chuck Liang began studying computer since the early 1980's. He received his BS degree from the University of Oregon in 1989 and Ph.D. from the University of Pennsylvania in 1995. He taught at the University of Delaware, Frostburg State University and Trinity College before coming to Hofstra University in year 2000, where he is currently Associate Professor. His research areas are in proof theory and the foundations of programming languages. In addition, he is also interested in computer networking, computer architecture, and distributed computing.