<\/p>\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
<\/em><\/p>\n[\/et_pb_text][\/et_pb_column][\/et_pb_row][et_pb_row column_structure=”2_5,3_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_column type=”2_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_image src=”https:\/\/easyconferences.eu\/fscd2023\/wp-content\/uploads\/2023\/05\/jdsj.jpg” title_text=”jdsj” align=”center” _builder_version=”4.20.2″ _module_preset=”default” width=”41%” global_colors_info=”{}”][\/et_pb_image][\/et_pb_column][et_pb_column type=”3_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_text _builder_version=”4.20.2″ _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>\nTitle: How can we trust AI?<\/p>\n
Abstract: 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: Mateja Jamnik is Professor of Artificial Intelligence at the University of Cambridge, UK. She is developing AI techniques for human-like computing \u2013 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
[\/et_pb_text][\/et_pb_column][\/et_pb_row][et_pb_row column_structure=”2_5,3_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_column type=”2_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_image src=”https:\/\/easyconferences.eu\/fscd2023\/wp-content\/uploads\/2023\/04\/manzone.jpg” title_text=”manzone” align=”center” _builder_version=”4.20.2″ _module_preset=”default” width=”41%” global_colors_info=”{}”][\/et_pb_image][\/et_pb_column][et_pb_column type=”3_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_text _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”]<\/p>\n
Giulio Manzonetto<\/h2>\n
LIPN&CNRS, Universit\u00e9 Sorbonne Paris Nord<\/em><\/p>\n<\/span><\/em><\/p>\nTitle: A Lambda Calculus Satellite<\/p>\n
Abstract: Barendregt\u2019s book “The Lambda Calculus, its syntax and semantics”
(1981\/84) has become a ‘classic’ in Theoretical Computer Science because it presents the state of the art in lambda calculus at that time in a comprehensive way. Moreover, a number of open problems and conjectures were proposed. In 2022, Barendregt and Manzonetto published a ‘sequel’ of this book, presenting the solutions of several of these problems, and more. In this talk, I will present a selection of these problems and the key ingredients that were employed in their solutions.<\/p>\n
[\/et_pb_text][\/et_pb_column][\/et_pb_row][et_pb_row column_structure=”2_5,3_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_column type=”2_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_image src=”https:\/\/easyconferences.eu\/fscd2023\/wp-content\/uploads\/2023\/05\/akihisa.jpg” title_text=”akihisa” align=”center” _builder_version=”4.20.2″ _module_preset=”default” width=”41%” global_colors_info=”{}”][\/et_pb_image][\/et_pb_column][et_pb_column type=”3_5″ _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_text _builder_version=”4.20.2″ _module_preset=”default” global_colors_info=”{}”]<\/p>\n
Akihisa Yamada<\/h2>\n
Cyber Physical Security Research Center, National Institute of Advanced Industrial Science and Technology (AIST)<\/em><\/p>\n<\/span><\/em><\/p>\nTitle: Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition<\/p>\n
Abstract: Automated termination analysis is a central topic in the research of term rewriting. In this talk, I will first review the theoretical foundation of termination of term rewriting, leading to the recently established tuple interpretation method. Then I will present an Isabelle\/HOL formalization of the theory. Although the formalization is based on the existing library IsaFoR (Isabelle Formalization of Rewriting), the present work takes another approach of representing relations (predicates rather than sets) so that the notation is more human friendly.<\/p>\n
Then I will present a unified implementation of the termination analysis techniques via SMT encoding, leading to the termination prover NaTT. Many tools have been developed for termination analysis and have been competing annually in termCOMP (Termination Competition) for two decades. At the end of the talk, I will share my experience in organizing termCOMP in the last five years.<\/p>\n
<\/p>\n
[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"
Keynote SpeakersMaribel Fernandez (Joint FSCD-CADE) King\u2019s College London Title: Nominal Techniques for Software Specification and Verification Abstract: 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 […]<\/p>\n","protected":false},"author":2,"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\/fscd2023\/wp-json\/wp\/v2\/pages\/12"}],"collection":[{"href":"https:\/\/easyconferences.eu\/fscd2023\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/easyconferences.eu\/fscd2023\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/fscd2023\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/fscd2023\/wp-json\/wp\/v2\/comments?post=12"}],"version-history":[{"count":18,"href":"https:\/\/easyconferences.eu\/fscd2023\/wp-json\/wp\/v2\/pages\/12\/revisions"}],"predecessor-version":[{"id":243755,"href":"https:\/\/easyconferences.eu\/fscd2023\/wp-json\/wp\/v2\/pages\/12\/revisions\/243755"}],"wp:attachment":[{"href":"https:\/\/easyconferences.eu\/fscd2023\/wp-json\/wp\/v2\/media?parent=12"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}