{"id":1788,"date":"2026-06-23T20:32:00","date_gmt":"2026-06-23T20:32:00","guid":{"rendered":"https:\/\/synasc.ro\/2026\/?page_id=1788"},"modified":"2026-06-23T20:34:01","modified_gmt":"2026-06-23T20:34:01","slug":"dorel-lucanu","status":"publish","type":"page","link":"https:\/\/synasc.ro\/2026\/invited-speakers\/dorel-lucanu\/","title":{"rendered":"Dorel Lucanu"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"1788\" class=\"elementor elementor-1788\" data-elementor-post-type=\"page\">\n\t\t\t\t<div class=\"elementor-element elementor-element-3e0b8ee e-con-full e-flex e-con e-parent\" data-id=\"3e0b8ee\" data-element_type=\"container\">\n\t\t\t\t<div class=\"elementor-element elementor-element-a3ba736 elementor-widget elementor-widget-heading\" data-id=\"a3ba736\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Matching-Logic-Based Domain Specific Reasoning<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-80ba9f5 elementor-widget elementor-widget-heading\" data-id=\"80ba9f5\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Dorel Lucanu<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-7088b6b elementor-widget elementor-widget-text-editor\" data-id=\"7088b6b\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>Faculty of Computer Science<br \/>Alexandru Ioan Cuza University of Ia\u0219i, Romania<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-6af37d1 elementor-widget elementor-widget-image\" data-id=\"6af37d1\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<img fetchpriority=\"high\" decoding=\"async\" width=\"300\" height=\"291\" src=\"https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/dl-synasc-300x291.png\" class=\"attachment-medium size-medium wp-image-1790\" alt=\"\" srcset=\"https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/dl-synasc-300x291.png 300w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/dl-synasc-1024x993.png 1024w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/dl-synasc-768x744.png 768w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/dl-synasc.png 1274w\" sizes=\"(max-width: 300px) 100vw, 300px\" \/>\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-6e257af elementor-align-center elementor-hidden-widescreen elementor-hidden-desktop elementor-hidden-tablet elementor-hidden-mobile elementor-icon-list--layout-traditional elementor-list-item-link-full_width elementor-widget elementor-widget-icon-list\" data-id=\"6e257af\" data-element_type=\"widget\" data-widget_type=\"icon-list.default\">\n\t\t\t\t\t\t\t<ul class=\"elementor-icon-list-items\">\n\t\t\t\t\t\t\t<li class=\"elementor-icon-list-item\">\n\t\t\t\t\t\t\t\t\t\t\t<a href=\"#\">\n\n\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-icon-list-icon\">\n\t\t\t\t\t\t\t<svg aria-hidden=\"true\" class=\"e-font-icon-svg e-fas-globe\" viewBox=\"0 0 496 512\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\"><path d=\"M336.5 160C322 70.7 287.8 8 248 8s-74 62.7-88.5 152h177zM152 256c0 22.2 1.2 43.5 3.3 64h185.3c2.1-20.5 3.3-41.8 3.3-64s-1.2-43.5-3.3-64H155.3c-2.1 20.5-3.3 41.8-3.3 64zm324.7-96c-28.6-67.9-86.5-120.4-158-141.6 24.4 33.8 41.2 84.7 50 141.6h108zM177.2 18.4C105.8 39.6 47.8 92.1 19.3 160h108c8.7-56.9 25.5-107.8 49.9-141.6zM487.4 192H372.7c2.1 21 3.3 42.5 3.3 64s-1.2 43-3.3 64h114.6c5.5-20.5 8.6-41.8 8.6-64s-3.1-43.5-8.5-64zM120 256c0-21.5 1.2-43 3.3-64H8.6C3.2 212.5 0 233.8 0 256s3.2 43.5 8.6 64h114.6c-2-21-3.2-42.5-3.2-64zm39.5 96c14.5 89.3 48.7 152 88.5 152s74-62.7 88.5-152h-177zm159.3 141.6c71.4-21.2 129.4-73.7 158-141.6h-108c-8.8 56.9-25.6 107.8-50 141.6zM19.3 352c28.6 67.9 86.5 120.4 158 141.6-24.4-33.8-41.2-84.7-50-141.6h-108z\"><\/path><\/svg>\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-icon-list-text\">Webpage<\/span>\n\t\t\t\t\t\t\t\t\t\t\t<\/a>\n\t\t\t\t\t\t\t\t\t<\/li>\n\t\t\t\t\t\t<\/ul>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-89d48db elementor-widget elementor-widget-heading\" data-id=\"89d48db\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">ABSTRACT<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-dd1252a elementor-widget elementor-widget-text-editor\" data-id=\"dd1252a\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>Matching logic (ML) is a minimal, foundational logic built around the notion of patterns \u2014 formulas interpreted as sets of elements \u2014 with native support for a least-fixpoint operator. Its expressive power and uniform treatment of structure and constraints make it a compelling substrate for domain-specific reasoning.<\/p><p>In this talk, we show how matching logic serves as a unifying foundation for inference systems across several domains. We begin with a self-contained introduction to matching logic: its syntax, semantics, and proof system. We then develop three case studies: (1) initial algebra semantics, where structural induction and primitive recursion are derived as theorems within matching logic rather than imposed as external rules; (2) rewrite-theory-generic reachability logic, where constrained constructor patterns are faithfully captured as matching logic theories; and (3) the K framework, where high-level language definitions are formally translated into matching logic theories, providing a rigorous denotational semantics for the K frontend.<\/p><p>Together, these results demonstrate that matching logic is a practical platform for deriving and certifying domain-specific reasoning systems within a single logical framework.<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-8c706e9 elementor-widget elementor-widget-heading\" data-id=\"8c706e9\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">SHORT BIO<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-0b87dae elementor-widget elementor-widget-text-editor\" data-id=\"0b87dae\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>Dorel Lucanu is a Romanian computer scientist and professor at the Faculty of Computer Science, Alexandru Ioan Cuza University of Ia\u0219i. His work focuses on formal methods, programming languages, software engineering, logics, rewriting systems, and the interaction between AI and formal methods. He has major contributions to the development of the Circ prover and K Framework.<\/p><p>He earned a Ph.D. in Computer Science from the Institute of Mathematics of the Romanian Academy in 1994 and obtained habilitation-equivalent Ph.D. supervision status at Alexandru Ioan Cuza University in 2007. He has taught programming, algorithms, and formal methods in software engineering at the Faculty of Computer Science since its founding in 1992.<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>Matching-Logic-Based Domain Specific Reasoning Dorel Lucanu Faculty of Computer ScienceAlexandru Ioan Cuza University of Ia\u0219i, Romania Webpage ABSTRACT Matching logic (ML) is a minimal, foundational logic built around the notion of patterns \u2014 formulas interpreted as sets of elements \u2014 with native support for a least-fixpoint operator. Its expressive power and uniform treatment of structure [&hellip;]<\/p>\n","protected":false},"author":30,"featured_media":0,"parent":226,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-1788","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1788","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/users\/30"}],"replies":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/comments?post=1788"}],"version-history":[{"count":4,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1788\/revisions"}],"predecessor-version":[{"id":1793,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1788\/revisions\/1793"}],"up":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/226"}],"wp:attachment":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/media?parent=1788"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}