Title: RTac — A Reflective Tactic Language

Abstract:

In this talk I will present RTac. RTac is a reflective tactic language in Coq that allows users to build decision procedures as Gallina programs in Coq. As a case study we have created sound decision procedures that verify Java programs using Separation Logic. These procedures can either succeed, fail, or partially succeed in which case a proof obligation is returned to the user. The main advantages that reflective decision procedures provide are two fold. The first is speed. Our decision procedures are several orders of magnitude faster than the corresponding procedures written in Coq’s native tactic language LTac. The second, in the case of RTac, is generality. Current reflective decision procedures written for Coq are highly specialised for e.g. for Presburger arithmetic or solving entailments in a logic. RTac is much more general and provides support for rewriting, lemma application and unification allowing us to create single tactics for complex compound problems like program verification.

About the speaker: http://www.itu.dk/people/jebe/