{"id":12,"date":"2020-06-03T07:46:53","date_gmt":"2020-06-03T07:46:53","guid":{"rendered":"http:\/\/easyconferences.eu\/itp2021\/?page_id=12"},"modified":"2023-07-03T19:55:14","modified_gmt":"2023-07-03T19:55:14","slug":"keynote-speakers","status":"publish","type":"page","link":"https:\/\/easyconferences.eu\/cade2023\/keynote-speakers\/","title":{"rendered":"Keynote Speakers"},"content":{"rendered":"

[et_pb_section fb_built=”1″ next_background_color=”#ffffff” _builder_version=”4.16″ background_color=”#8c8c8c” top_divider_color=”#b53319″ bottom_divider_style=”arrow3″ global_colors_info=”{}”][et_pb_row _builder_version=”4.16″ custom_margin=”-26px|auto||auto||” global_colors_info=”{}”][et_pb_column type=”4_4″ _builder_version=”4.16″ global_colors_info=”{}”][et_pb_text _builder_version=”4.16″ global_colors_info=”{}”]<\/p>\n

Keynote Speakers<\/span><\/h2>\n

[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section fb_built=”1″ _builder_version=”4.16″ global_colors_info=”{}”][et_pb_row column_structure=”1_3,2_3″ _builder_version=”4.20.4″ _module_preset=”default” custom_padding=”8px|||||” global_colors_info=”{}”][et_pb_column type=”1_3″ _builder_version=”4.17.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_image src=”https:\/\/easyconferences.eu\/cade2023\/wp-content\/uploads\/2023\/04\/image.webp” title_text=”image” align=”center” _builder_version=”4.20.4″ _module_preset=”default” global_colors_info=”{}”][\/et_pb_image][\/et_pb_column][et_pb_column type=”2_3″ _builder_version=”4.17.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_text _builder_version=”4.20.4″ _module_preset=”default” global_colors_info=”{}”]<\/p>\n

Jasmin Christian Blanchette<\/h1>\n

Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen<\/em><\/p>\n

Lambda-Superposition: From Theory to Trophy<\/em><\/h3>\n

Abstract:<\/strong> Lambda-superposition is a proof calculus for higher-order logic (simple type theory) developed in collaboration with Alexander Bentkamp, Simon Cruanes, Visa Nummelin, Sophie Tourret, Petar Vukmirovi\u0107, and Uwe Waldmann. To a large extent, the calculus is a graceful generalization of standard superposition, which is a highly successful calculi for first-order logic. On the theory side, we proved the lambda-superposition refutationally complete. On the practical side, we implemented it in the Zipperposition prover and, together with Stephan Schulz, in the E prover. Zipperposition finished first in the higher-order theorem division of the CADE ATP System Competition in 2020, 2021, and 2022, suggesting that superposition is a valuable approach also in a higher-order setting.<\/p>\n

Bio:<\/strong> Jasmin Blanchette is holder of the Chair of Theoretical Computer Science at Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen. His research focuses on the use and development of proof assistants and automatic theorem provers. On the proof assistant front, he (co)developed three tools for the Isabelle\/HOL proof assistant: the Nitpick model finder, the Sledgehammer proof tool, and the (co)datatype package. On the automatic theorem proving front, he and his colleagues developed lambda-superposition. He also applied proof assistants to verify the correctness of the logical calculi underlying automatic provers.<\/p>\n

[\/et_pb_text][\/et_pb_column][\/et_pb_row][et_pb_row column_structure=”1_3,2_3″ _builder_version=”4.20.4″ _module_preset=”default” custom_padding=”8px|||||” global_colors_info=”{}”][et_pb_column type=”1_3″ _builder_version=”4.17.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_image src=”https:\/\/easyconferences.eu\/cade2023\/wp-content\/uploads\/2023\/04\/maribel-fernandez-web.x086327cc.webp” title_text=”maribel-fernandez-web.x086327cc” align=”center” _builder_version=”4.20.4″ _module_preset=”default” global_colors_info=”{}”][\/et_pb_image][\/et_pb_column][et_pb_column type=”2_3″ _builder_version=”4.17.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_text _builder_version=”4.21.0″ _module_preset=”default” global_colors_info=”{}”]<\/p>\n

Maribel Fernandez (Joint FSCD-CADE)<\/h1>\n

King’s College London<\/em><\/p>\n

Nominal Techniques for Software Specification and Verification<\/h3>\n

Abstract:<\/strong> The nominal approach to the specification of languages with binding operators, introduced by Gabbay and Pitts, has its roots in nominal set theory. With a user-friendly first-order syntax, nominal logic provides a formal framework to reason about binding operators similar to conventional, on-paper reasoning. Indeed, nominal logic uses the well-understood concept of permutation groups acting on sets to provide a rigorous first-order treatment for the common informal practice of fresh and bound names.\u00a0<\/p>\n

In this talk, I will present our current work towards incorporating nominal techniques into two widely-used rule-based first-order verification environments: the K specification framework and the Maude programming environment. Read More<\/a><\/span>\n

\u00a0<\/span><\/p>\n
\n

An important component of rule-based programming and verification environments is the unification algorithm used to solve equational problems. In practice, unification problems are solved in the context of equational axioms. In the first part of the talk we will discuss nominal unification modulo equational theories. In particular, we will discuss nominal unification modulo associativity and commutativity, and the use of nominal narrowing to deal with theories presented by convergent rewrite rules.\u00a0<\/p>\n

Another important component of verification environments is the type system. In the second part of the talk we will discuss type systems for nominal languages (including polymorphic systems and \u00a0intersection systems). Dependent type theories, the dominant approach to formalising programming languages, have also been extended with nominal features. \u00a0A lambda-less nominal dependent type system is available and we are currently working on a type checker for this system.\u00a0<\/p>\n

The talk will be structured as follows: we will start with the definition of nominal logic (including the notions of fresh atoms and alpha-equivalence) followed by a brief introduction to nominal matching and unification. We will then define nominal rewriting, a generalisation of \u00a0first-order rewriting that provides in-built support for alpha-equivalence following the nominal approach. Finally, we will discuss notions of nominal unification and rewriting modulo associative and commutative operators and briefly overview typed versions of nominal languages.<\/div><\/p>\n<\/div>\n

[\/et_pb_text][\/et_pb_column][\/et_pb_row][et_pb_row column_structure=”1_3,2_3″ _builder_version=”4.20.4″ _module_preset=”default” custom_padding=”8px|||||” global_colors_info=”{}”][et_pb_column type=”1_3″ _builder_version=”4.17.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_image src=”https:\/\/easyconferences.eu\/cade2023\/wp-content\/uploads\/2023\/05\/Mateja-Jamnik.png” title_text=”Mateja Jamnik” align=”center” _builder_version=”4.21.0″ _module_preset=”default” global_colors_info=”{}”][\/et_pb_image][\/et_pb_column][et_pb_column type=”2_3″ _builder_version=”4.17.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_text _builder_version=”4.20.4″ _module_preset=”default” global_colors_info=”{}”]<\/p>\n

Mateja Jamnik (Joint FSCD-CADE)<\/h1>\n

University of Cambridge, UK (Department of Computer Science and Technology)<\/em><\/p>\n

How Can We Make Trustworthy AI?<\/h3>\n

Abstract:<\/strong> Not too long ago most headlines talked about our fear of AI. Today, AI is ubiquitous, and the conversation has moved on from whether we should use AI to how we can trust the AI systems that we use in our daily lives. In this talk I look at some key technical ingredients that help us build confidence and trust in using intelligent technology. I argue that intuitiveness, interaction, explainability and inclusion of human domain knowledge are essential in building this trust. I present some of the techniques and methods we are building for making AI systems that think and interact with humans in more intuitive and personalised ways, enabling humans to better understand the solutions produced by machines, and enabling machines to incorporate human domain knowledge in their reasoning and learning processes.<\/p>\n

Bio:<\/strong> Mateja Jamnik is Professor of Artificial Intelligence at the University of Cambridge, UK. She is developing AI techniques for human-like computing – she combines AI reasoning with machine learning techniques in order to advance the explainability of AI systems, and applies them to personalised medicine and tutoring systems. Mateja is passionate about bringing science closer to the public and engages frequently with the media and outreach events. She has been advising the UK government on policy direction in relation to the impact of AI on society.<\/p>\n

<\/em><\/p>\n

[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"

Keynote SpeakersJasmin Christian Blanchette Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen Lambda-Superposition: From Theory to Trophy Abstract: Lambda-superposition is a proof calculus for higher-order logic (simple type theory) developed in collaboration with Alexander Bentkamp, Simon Cruanes, Visa Nummelin, Sophie Tourret, Petar Vukmirovi\u0107, and Uwe Waldmann. To a large extent, the calculus is a graceful generalization of standard superposition, which is […]<\/p>\n","protected":false},"author":3,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"","_et_gb_content_width":""},"_links":{"self":[{"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/pages\/12"}],"collection":[{"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/comments?post=12"}],"version-history":[{"count":18,"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/pages\/12\/revisions"}],"predecessor-version":[{"id":243804,"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/pages\/12\/revisions\/243804"}],"wp:attachment":[{"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/media?parent=12"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}