Dear colleagues, Do not miss the 4th Women in Logic Workshop, affiliated with the FSCD/IJCAR 2020.
*The Women in Logic workshop (WiL)* provides an opportunity to increase awareness of the valuable contributions made by women in the area of logic in computer science. Its main purpose is to promote the excellent research done by women, with the ultimate goal of increasing their visibility and representation in the community. The event is supported by the ACM SIGLOG, the Vienna Center for Logic and Algorithms (VCLA) and the Institute of Logic, Language and Computation of the University of Amsterdam (ILLC). *FREE REGISTRATION* (Everybody is welcome, *no matter the gender*): https://fscd-ijcar-2020.org/register-ws *KEYNOTE SPEAKERS* - *Maribel Fernández* <https://www.google.com/url?q=https%3A%2F%2Fnms.kcl.ac.uk%2Fmaribel.fernandez%2F&sa=D&sntz=1&usg=AFQjCNFDHRanHRsECH9dPbf88p4GxGIYyg>* (Kings College London)* *Title:* *Nominal Syntax with Atom Substitutions* *Abstract: *Unification and matching algorithms are essential components of logic and functional programming languages and theorem provers. Nominal extensions have been developed to deal with syntax involving binding operators: Nominal syntax is a generalisation of first-order syntax that includes names, a notion of name binding and an elegant axiomatisation of alpha-equivalence, based on nominal set theory. However, it does not take into account non-capturing atom substitution, which is not a primitive notion in nominal syntax. We consider an extension of nominal syntax with non-capturing atom substitutions and show that matching is decidable and finitary but unification is undecidable in general. The proof of undecidability of unification is obtained by reducing Hilbert's tenth problem to unification of extended nominal terms.We provide a general matching algorithm and characterise a class of problems for which matching is unitary, giving rise to expressive and efficient notions of rewriting. This is joint work with Jesus Dominguez. - *Alexandra Silva* <https://www.google.com/url?q=https%3A%2F%2Falexandrasilva.org%2F%23%2Fmain.html&sa=D&sntz=1&usg=AFQjCNH7GYLDidAMvpLxZCIo7jfq-TNztg>* (University College London)* *Title*: *An algebraic framework to reason about concurrency* *Abstract*: Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Hoare, Struth, and collaborators proposed a concurrent extension of Kleene Algebra (CKA) as a first step towards developing algebraic reasoning for concurrent programs. Completing their research program and extending KAT to encompass concurrent behaviour has however proven to be more challenging than initially expected. The core problem appears because when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation about programs. In this talk, we will revise the literature on CKA(T) and explain the challenges and solutions in the development of an algebraic framework for concurrency.The talk is based on a series of papers joint with Tobias Kappé, Paul Brunet, Bas Luttik, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi. Detailed references can be found on the CoNeCo project website: https://coneco-project.org/ <https://www.google.com/url?q=https%3A%2F%2Fconeco-project.org%2F&sa=D&sntz=1&usg=AFQjCNFW1Mj9rfLzvbzoYULbtneMUVfEWw> . *PROGRAM* The full program is available at: https://sites.google.com/g.uporto.pt/wil2020/programme?authuser=0 <https://sites.google.com/g.uporto.pt/wil2020/programme?authuser=0> -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/933b538d-e243-428d-a85e-8e6b4aefbd9do%40dimap.ufrn.br.
