{"id":88,"date":"2023-01-10T14:29:55","date_gmt":"2023-01-10T13:29:55","guid":{"rendered":"https:\/\/project.inria.fr\/unif2023\/?page_id=88"},"modified":"2023-08-23T14:55:35","modified_gmt":"2023-08-23T12:55:35","slug":"program","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/unif2023\/program\/","title":{"rendered":"Program"},"content":{"rendered":"\n<p class=\"wp-block-paragraph\">The program includes invited and contributed talks. The related extended abstracts can be found in the electronic <a href=\"https:\/\/inria.hal.science\/UNIF2023\">informal proceedings<\/a>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>(Tentative) Schedule:<\/strong><\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>09:00 &#8211; 10:00 Session 1 (Invited Talk)<\/em>. Chair: Veena Ravishankar\/Christophe Ringeissen<\/p>\n\n\n\n<ul class=\"wp-block-list\"><li>(09:00) Mauricio Ayala-Rinc\u00f3n (Universidade de Bras\u00edlia). <strong><a href=\"https:\/\/inria.hal.science\/hal-04137801\">Formalisation of Nominal Equational Reasoning<\/a><\/strong> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_Ayala.pdf\">slides<\/a>)<\/li><\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><em>10:00 &#8211; 10:30 Coffee Break<\/em><\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>10:30 &#8211; 12:30 Session 2<\/em>. Chair: David Cerna<\/p>\n\n\n\n<ul class=\"wp-block-list\"><li>(10:30) Sam van Gool\u00a0and\u00a0Johannes Marti.\u00a0<a href=\"https:\/\/inria.hal.science\/hal-04128087\">Modal unification step by step<\/a> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_5.pdf\">slides<\/a>)<\/li><li>(11:00) St\u00e9phane P. Desarzens.\u00a0<a href=\"https:\/\/inria.hal.science\/hal-04128048\">One-Variable Unification in K<\/a> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_3.pdf\">slides<\/a>)<\/li><li>(11:30) Aleksy Schubert.\u00a0<a href=\"https:\/\/inria.hal.science\/hal-04128012\">Second-order unification and functional arity<\/a> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_2.pdf\">slides<\/a>)<\/li><li>(12:00) Nikolai Kudasov.\u00a0<a href=\"https:\/\/inria.hal.science\/hal-04128229\">Generalising Huet-style Projections in E-unification for Second-Order Abstract Syntax<\/a> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_9.pdf\">slides<\/a>)<\/li><\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><em>12:30 &#8211; 14:00 Lunch Break<\/em><\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>14:00 &#8211; 15:30 Session 3<\/em>. Chair: Andrew Marshall<\/p>\n\n\n\n<ul class=\"wp-block-list\"><li>(14:00) Jo\u00e3o Barbosa,&nbsp;M\u00e1rio Florido&nbsp;and&nbsp;Vitor Santos-Costa.&nbsp;<a href=\"https:\/\/inria.hal.science\/hal-04127949\">Typed Unification: when failure may not be wrong<\/a> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_1.pdf\">slides<\/a>)<\/li><li>(14:30) Wei Du, Paliath Narendran and Michael Rusinowitch.&nbsp;<a href=\"https:\/\/inria.hal.science\/hal-04128213\">Inferring RPO Symbol Ordering<\/a> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_7.pdf\">slides<\/a>)<\/li><li>(15:00) Georg Ehling and Temur Kutsia.&nbsp;<a href=\"https:\/\/inria.hal.science\/hal-04128216\">Matching in Quantitative Equational Theories<\/a> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_8.pdf\">slides<\/a>)<\/li><\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><em>15:30 &#8211; 16:00 Coffee Break<\/em><\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>16:00 &#8211; 17:00 Session 4 (Invited Talk)<\/em>. Chair: Temur Kutsia<\/p>\n\n\n\n<ul class=\"wp-block-list\"><li>(16:00) Deepak Kapur (UNM, Albuquerque). <strong><a href=\"https:\/\/inria.hal.science\/hal-04143456\">Invariant Generation as Semantic Unification: <strong>A New Perspective<\/strong><\/a><\/strong><\/li><\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><em>17:00 &#8211; 18:00 Session 5<\/em>. Chair: Daniele Nantes-Sobrinho<\/p>\n\n\n\n<ul class=\"wp-block-list\"><li>(17:00) Andr\u00e9s Felipe Gonz\u00e1lez Barrag\u00e1n, David Cerna, Mauricio Ayala-Rinc\u00f3n and Temur Kutsia. <a href=\"https:\/\/hal.science\/hal-04128203\">On Anti-unification in Absorption Theories<\/a> (<a href=\"https:\/\/members.loria.fr\/CRingeissen\/files\/UNIF2023\/UNIF_2023_slides_6.pdf\">slides<\/a>)<\/li><li>(17:30) Andrew Pulver.&nbsp;The conjugacy problem and the uniform common term problem in dwindling string rewriting systems. Abstract: <em>In this paper we investigate the conjugacy problem and the uniform common term problem in the context of &#8220;dwindling&#8221; string rewriting systems. The conjugacy problem is shown to be solvable in polynomial time, and the uniform common term problem is shown to be undecidable. Several basic properties of dwindling string rewriting systems are demonstrated (extended abstract to appear in the informal proceedings).<\/em><\/li><\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Invited Talks:<\/strong><\/p>\n\n\n\n<ul class=\"wp-block-list\"><li>Mauricio Ayala-Rinc\u00f3n (Universidade de Bras\u00edlia). <strong>Formalisation of Nominal Equational Reasoning<\/strong>. Abstract: <em>In contrast to other methods to bind variables, the nominal approach uses atoms and the algebra of atom permutations bringing enlightening implications. This talk will discuss the lessons learned from our experience towards formalising nominal matching and nominal unification modulo C and AC using the proof assistant PVS (Prototype Verification System). Furthermore, the talk will dissect exciting issues that appear during the formalisation of nominal equational reasoning giving rise to surprises regarding the well-known properties of first-order unification and unification modulo C and AC.<\/em><\/li><li>Deepak Kapur (UNM, Albuquerque).<strong> Invariant Generation as Semantic Unification<\/strong>: <strong>A New Perspective<\/strong>. Abstract: <em>Unification is the problem of finding instantiations of variables in a finite set of equations constructed using function symbols such that both sides of the instantiated equations are equal. In semantic unification, also called E-unification, function symbols can have properties specified typically by an equational theory; a unifier then makes the two instantiated sides of each equation, equivalent modulo the equation theory. By generalizing the unification problem to a first-order theory in which variables in the problem stand for formulas in the theory, the invariant generation problem in software, hardware, and cyber-physical system can be formulated as a unification problem. Finding a nontrivial unifier in this case amounts to finding an invariant which is a formula in the theory. Similarly, finding a most general unifier in that theory amounts to finding the strongest invariant. Instantiation of variables can be further restricted to formulas with certain shapes\/properties. A number of examples from the literature of the automatic generation of loop invariants in software will be used to illustrate this new perspective<\/em>.<\/li><\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Accepted Contributions:<\/strong><\/p>\n\n\n\n<ul class=\"wp-block-list\"><li>Jo\u00e3o Barbosa,&nbsp;M\u00e1rio Florido&nbsp;and&nbsp;Vitor Santos-Costa.&nbsp;Typed Unification: when failure may not be wrong<\/li><li>Aleksy Schubert.&nbsp;Second-order unification and functional arity<\/li><li>St\u00e9phane P. Desarzens.&nbsp;One-Variable Unification in K<\/li><li>Sam van Gool&nbsp;and&nbsp;Johannes Marti.&nbsp;Modal unification step by step<\/li><li>Andr\u00e9s Felipe Gonz\u00e1lez Barrag\u00e1n, David Cerna, Mauricio Ayala-Rinc\u00f3n and Temur Kutsia.&nbsp;On Anti-unification in Absorption Theories<\/li><li>Wei Du, Paliath Narendran and Michael Rusinowitch.&nbsp;Inferring RPO Symbol Ordering<\/li><li>Georg Ehling and Temur Kutsia.&nbsp;Matching in Quantitative Equational Theories<\/li><li>Nikolai Kudasov.&nbsp;Generalising Huet-style Projections in E-unification for Second-Order Abstract Syntax<\/li><li>Andrew Pulver.&nbsp;The conjugacy problem and the uniform common term problem in dwindling string rewriting systems<\/li><\/ul>\n","protected":false},"excerpt":{"rendered":"<p>The program includes invited and contributed talks. The related extended abstracts can be found in the electronic informal proceedings. (Tentative) Schedule: 09:00 &#8211; 10:00 Session 1 (Invited Talk). Chair: Veena Ravishankar\/Christophe Ringeissen (09:00) Mauricio Ayala-Rinc\u00f3n (Universidade de Bras\u00edlia). Formalisation of Nominal Equational Reasoning (slides) 10:00 &#8211; 10:30 Coffee Break 10:30\u2026<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/unif2023\/program\/\"><span>Continue reading<\/span><i class=\"crycon-right-dir\"><\/i><\/a> <\/p>\n","protected":false},"author":2284,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":"","_members_access_role":[],"_members_access_error":""},"class_list":["post-88","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/unif2023\/wp-json\/wp\/v2\/pages\/88","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/unif2023\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/project.inria.fr\/unif2023\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/unif2023\/wp-json\/wp\/v2\/users\/2284"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/unif2023\/wp-json\/wp\/v2\/comments?post=88"}],"version-history":[{"count":28,"href":"https:\/\/project.inria.fr\/unif2023\/wp-json\/wp\/v2\/pages\/88\/revisions"}],"predecessor-version":[{"id":180,"href":"https:\/\/project.inria.fr\/unif2023\/wp-json\/wp\/v2\/pages\/88\/revisions\/180"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/unif2023\/wp-json\/wp\/v2\/media?parent=88"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}