Scottish Theorem Proving

News: We are very grateful to the SICSA Modeling and Abstraction theme for funding a meal for all attendees of our meeting!

There will be a meeting of STP in Edinburgh on Friday, 20th November, 2009, in the School of Informatics, University of Edinburgh, from 1:00 to 5:30 pm.

The meeting is in the combined rooms IF 4.31+4.33 of the Informatics Forum of the University of Edinburgh.

Address: Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK

Google Maps: Much information

Programme:

• 1:00-2:00: Catered lunch in Mini Forum 2 (IF 4.30)
  
• 2:00-3:00: J Strother Moore (University of Texas at Austin and University of Edinburgh; brief biography)
  • Title: Machines Reasoning about Machines
  • Abstract: Computer hardware and software can be modeled precisely in mathematical logic. If expressed appropriately, these models can be executable. This allows them to be used as simulation engines or rapid prototypes. But because they are formal they can be manipulated by symbolic means: theorems can be proved about them, directly, with mechanical theorem provers. But how practical is this vision of machines reasoning about machines? In this highly personal talk, I will describe the 38 year history of the ``Boyer-Moore Project,'' the current version of the prover (ACL2: A Computational Logic for Applicative Common Lisp by Kaufmann and Moore), and discuss progress toward making formal verification practical. ACL2 is an interactive automated theorem prover in which the user guides the system implicitly via the sequence of lemmas presented. It supports rule-based simplification, many decision procedures, mathematical induction, and a variety of other proof techniques. Among other examples I will describe important theorems about commercial microprocessor designs, including parts of processors by AMD, Motorola, IBM, Rockwell-Collins and others. Some of these microprocessor models execute at 90% the speed of C models and have had important functional properties verified. In addition, I will describe a model of the Java Virtual Machine, including class loading and bytecode verification and the proofs of theorems about JVM methods.
• 3:00-3:15 Coffee break (including 5-min SICSA Presentation by Jane Hillston)
  
• 3:15-3:45 Jamie Gabbay (Heriot-Watt University)
  • Title: Permissive Nominal Terms
  • Abstract: I will briefly survey the "nominal" literature and then describe recent work with Gilles Dowek and Dominic Mulligan aimed at developing an extension of first-order logic with names and binding, which we call Permissive Nominal Logic. This preserves the flavour of first-order logic and allows us to formalise the informal but rigorous meta-level in which specifications with names and binding such as those of the lambda-calculus and first- or higher-order logic, are given. Time permitting, I will discuss the potential applications of this to theorem-proving. Further details can also be found on my homepage.
• 3:45-4:00 Coffee break
  
• 4:00-4:30 Randy Pollack (University of Edinburgh)
  • Title: A Canonical Locally Named Representation of Binding (joint work with Masahiko Sato)
  • Abstract: Binding is fundamental in mathematics and computer science. We must be able to formally represent and reason about binding to carry out a program of mechanising metatheory in computer science. One broad approach uses distinct syntactic classes of "parameters" (used for free or globally bound variables) vs "local variables" (used for bound variables). This general idea, which we call local representation, goes back (informally) to Frege. In 1992 McKinna and Pollack formalised a local representation using distinct classes of names for parameters and variables. This representation is not canonical (terms have more than one representation) but much metatheory of Pure Type Systems was formalised without the need to reason about (or even define) alpha-equivalence. In the present work we give a refinement of McKinna--Pollack representation that is canonical. The central idea that makes this possible is due to Sato. The work is formalised in Nominal Isabelle. A full paper will appear in Journal of Symbolic Computation. Our ongoing work has improved upon this paper.
• 4:30-4:45 Short break
  
• 4:45-5:15 Grant Olney Passmore (University of Edinburgh)
  • Title: Recent Advances in Satisfiability Modulo Nonlinear Real Arithmetic (joint work with Leo de Moura)
  • Abstract: I will present some recent work (joint with Leo de Moura) on developing decision methods for nonlinear real arithmetic which are specialised to the needs of SMT (``SAT Modulo Theories'') solvers. At the foundation of this work is our new theory of ``strategy-independent Groebner bases,'' which I will motivate and outline at a high-level. Much of this work has been implemented by de Moura in the SMT solver Z3 available from Microsoft Research. Two recently published papers of ours relevant to this talk are ``Superfluous S-polynomials in Strategy-Independent Groebner Bases'' (SYNASC-2009) and ``On Locally Minimal Nullstellensatz Proofs'' (SMT-2009), both available from my website.


• 5:15-5:30 Closing + Heading to Dagda Bar ( info )

Organised by G. O. Passmore and L. Dixon and L. Georgieva
    email: {g DOT passmore AT ed.ac.uk, l DOT dixon AT ed.ac.uk, lilia AT macs.hw.ac.uk}.