Copenhagen Programming Language Seminar

Combining Deduction~Modulo and Logics of Fixed-Point Definitions

Gopalan Nadathur
University of Minnesota and IT University of Copenhagen

Friday, May 25th, 2012, 11:15 - 12:00
DIKU, Universitetsparken 1, Meeting room A+B


Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive specifications. These specifications are not directly complemented by fixed-point reasoning techniques and, correspondingly, do not have to satisfy strong monotonicity restrictions. We show how to incorporate a rewriting capability into logics of fixed-point definitions towards additionally supporting recursive specifications. Specifically, we describe a natural deduction calculus that adds a form of ``closed-world'' equality---a key ingredient to supporting fixed-point definitions---to deduction modulo a framework for extending a logic with a rewriting layer operating on formulas. Our calculus enjoys strong normalizability when the rewrite system satisfies general properties and we have shown its usefulness in formalizing arguments such as those based on logical relations. Our integration of closed-world equality into deduction modulo uses an elimination principle for this form of equality that, for the first time, allows us to require finiteness of proofs without sacrificing stability under reduction.

Scientific host: Fritz Henglein Administrative host:Jette Møller. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, DTU, ITU, and RUC.
COPLAS is part of the FIRST Research School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org