Abstract: This talk describes work in progress to develop a calculus for program verification in which implementations and specifications are both written in the untyped lambda calculus. Some existing program verification systems, notably Coq, also allow implementations and specifications to be written in the same (computational) language, but must restrict the language so that only terminating programs may be written (thus resulting in a loss of expressive power). The alternation calculus is based on an untyped lambda calculus with an intensional equality test. Its crucial novel feature is an alternation operator which dualizes termination and non-termination. If M diverges, then alt(M) terminates; and if M terminates, then alt(M) diverges. This operator cannot actually be implemented, of course, since termination is not decidable. Hence, as a programming language, the alternation calculus is idealized. Nevertheless, we show how it provides a computational interpretation of the logical connectives, and thus forms a basis for reasoning about programs. To avoid an impredicative operational semantics, the calculus is formalized in terms of limits of finite approximate computations. This requires new kinds of meta-theorems than those usual in programming languages theory. This motivates developing the meta-theory in a proof assistant, namely Coq. The talk presents techniques for formalizing meta-theory, particularly to deal with binders, which the speaker has used in a solution to part 1 of the POPLmark challenge (which calls for the formalization of programming languages meta-theory in proof assistants).

Bio: Aaron Stump is an assistant professor in the Computer Science and Engineering Department at Washington University in St. Louis. He got his PhD in Computer Science in 2002 from Stanford University. His research interests are in computational logic, programming languages theory and automated reasoning. His work is currently supported by a National Science Foundation CAREER award entitled "Semantic Programming."

-- Main.EmirPasalic - 05 Apr 2006