Session Chair: E. Clarke.

Speaker: Gérard Huet, INRIA Rocquencourt.

Title: Design of a Proof Assistant.

Abstract: We discuss a few architectural design decisions for a general purpose proof assistant, combining a programmable tactics-based proof-checker, a sequent calculus search engine based on logic programming with higher-order unification constraints, a library browser managing modular mathematical developments, and a user interface allowing structural selection in formulas displayed in readable notation. The talk is illustrated with concrete experience issued from various versions of the Coq Proof Assistant for Type Theory. It is intended as a discussion platform for the QED collaborative endeavor.

Biographical Sketch: Gérard Huet worked for the last 25 years in the area of applying formal tools from algebra and logic to computer science problems, ranging from semantics of programming languages and design of logical frameworks to more applied areas such as implementing programming environments, functional languages and proof systems. He worked in particular on lambda-calculus, type theory, higher-order unification, confluence and sequentiality of rewrite systems, and type-theoretic specification languages. He is the co-designer and author of the Mentor programming environment, the CAML programming language, and the Coq Proof Assistant. Gérard Huet is correspondant de l'Academie des Sciences, member of Academia Europaea. He is Directeur de Recherches at INRIA (French National Research Institute in Computer Science and Control), Rocquencourt branch.