BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Synthesis of Second-Order Equational Logic - Marcelo Fiore (Univer
 sity of Cambridge)
DTSTART:20081028T141500Z
DTEND:20081028T154500Z
UID:TALK14787@talks.cam.ac.uk
CONTACT:Richard Garner
DESCRIPTION: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].\n\nAs a running example\, I w
 ill indicate how the methodology applies to rationally reconstruct the tra
 ditional equational logic of universal algebra from categorical principles
 \; see [3 (Part I)].\n\nAs for a modern application\, I will use the metho
 dology to synthesise a second-order equational logic for specifying simple
  type theories\; see [2 (Part I)] and [3 (Part II)].\n\nThis is joint work
  with Chung-Kil Hur.\n\nReferences\n\n[1] Marcelo Fiore and Chung-Kil Hur.
   _Term equational systems and logics._  In 24th Mathematical Foundations 
 of Programming Semantics Conf. (MFPS XXIV)\, 2008.\n\n"Paper":http://www.c
 l.cam.ac.uk/~mpf23/papers/Categories/TESL.pdf\n\n[2] Marcelo Fiore.  _Seco
 nd-order and dependently-sorted abstract syntax._  In Logic in Computer Sc
 ience Conf. (LICS'08)\, pages 57-68. IEEE\, Computer Society Press\, 2008.
 \n\n"Paper":http://www.cl.cam.ac.uk/~mpf23/papers/Types/AbsSyn.pdf\n\n"Sli
 des":http://www.cl.cam.ac.uk/~mpf23/papers/Types/LiCS08.pdf\n\n[3] Marcelo
  Fiore.  _Algebraic theories and equational logics._ Invited tutorial at t
 he 24th Mathematical Foundations of Programming Semantics Conf. (MFPS XXIV
 )\, 2008.\n\n"Notes":http://www.cl.cam.ac.uk/~mpf23/Notes/atel.pdf\n
LOCATION:MR9\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR