The date for the annunal meeting WG 1.6 is Sunday, June 26, 2016. WG 1.6 will be part of FSCD and it will take place one day after the main conference.
Abstract: One context unification extends first-order unification by introducing a single context variable, possibly with multiple occurrences. One context unification is known to be in NP, but it is not known to be solvable in polynomial time. In this talk, we present a polynomial time algorithm for certain interesting classes of the one context unification problem. Our algorithm is presented as an inference system that non-trivially extends the usual inference rules for first-order unification. The algorithm is of independent value as it can be used, with slight modifications, to solve other problems, such as the first-order unification problem that tolerates one clash.
Abstract: Coinduction is a key proof technique to establish properties about systems that continue to run and produce results (i.e. network or communications protocols, I/O interaction, data streams, or processes) . Yet, mechanizing coinductive proofs about formal systems and representing, generating and manipulating such proofs remains challenging. In this talk, we develop the idea of programming coinductive proofs dual to the idea of programming inductive proofs. Unlike properties about finite data which can be defined by constructing a derivation, properties about infinite data can be described by the possible observations we can make. Dual to pattern matching, a tool for analyzing finite data, we develop the concept of copattern matching, which allows us to describe properties about infinite data. This leads to a symmetric proof language where pattern matching on finite and infinite data can be mixed.
This is joint work with Andreas Abel, Andrew Cave, David Thibodeau, Anton Setzer.The meetings of the working group are public, with the single exception of the business meeting.