Abstract

I will present a mathematical methodology for the synthesis of equational deduction systems that are sound and internally complete for a canonical algebraic model theory; see [1].

As a running example, I will indicate how the methodology applies to rationally reconstruct the traditional equational logic of universal algebra from categorical principles; see [3 (Part I)].

As for a modern application, I will use the methodology to synthesise a second-order equational logic for specifying simple type theories; see [2 (Part I)] and [3 (Part II)].

This is joint work with Chung-Kil Hur.

References

[1] Marcelo Fiore and Chung-Kil Hur. Term equational systems and logics. In 24th Mathematical Foundations of Programming Semantics Conf. (MFPS XXIV ), 2008.

Paper

[2] Marcelo Fiore. Second-order and dependently-sorted abstract syntax. In Logic in Computer Science Conf. (LICS’08), pages 57-68. IEEE , Computer Society Press, 2008.

Paper

Slides

[3] Marcelo Fiore. Algebraic theories and equational logics. Invited tutorial at the 24th Mathematical Foundations of Programming Semantics Conf. (MFPS XXIV ), 2008.

Notes