STEP-2023

  

Российский гибридный семинар STEP-2023
по фундаментальным вопросам программной инженерии,
теории и экспериментальному программированию (2023 г):
STEP = Software Engineering, Theory and Experimental Programming.

Семинар STEP-2023 был продолжением в 2023 г. семинара ru-STEP, созданного в 2020 г. В 2024 г. работает семинар STEP-2024.

Программный Комитет семинара STEP-2023:

Общие сведения о семинаре:

  • Семинар является продолжением семинара ru-STEP, созданного в 2020 г. инициативой группой сотрудников Университета Иннополис и Института систем информатики им. А.П. Ершова.
  • Периодичность заседаний семинара - 1 раз в две недели, расписание формируется в начале каждого семестра Программным Комитетом семинара, программа семинара формируется на месяц вперед Программным Комитетом и публикуется на данной странице.
  • Видеоархив семинара размещается в плейлисте на YouTube-канале ИСИ СО РАН (то есть, продолжает видеоархив семинара ru-STEP).
  • Язык семинара русский и английский. Рекомендуется готовить презентацию на английском, доклад и обсуждение делать на русском (если нет зарубежных участников), но быть готовым перейти на английский (если есть зарубежные участники).
  • Программный Комитет имеет намерение подготовить и публиковать обзоры докладов, представленных на семинаре. (Обзор Running Regular Research Seminar Online работы семинара ru-STEP за 2020-22 гг. опубликован в 2023 г.)

Прошедшие заседания семинара: (в порядке Last-In - First-Out):

Заключительная встреча семинара в 2023 г. - традиционный предновогодний День Проблем STEP-2023 продолжbk традицию семинара ru-STEP и провел в канун нового 2024 года традиционный День Проблем (см. "День Проблем 2020", "День Проблем 2021" и "День Проблем 2022").
Выступили: 		Дата: пятница 30 декабря 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. Есть презентации выступлений И.С. Ануреева, Д.А. Кондратьева, А.В. Коновалова, , А.Н. Непейвода и Н.В. Шилова.
Николай Николаевич Ефанов (Московский физико-технический институт): Software optimization gaining by middle-end compiler phase-ordering: actual state and directions Аннотация: The report is devoted to the actual state and problems of software optimization using compiler auto-tuning approaches with middle-end optimization phase-ordering. First of all, the main methodics and entities of this technical research field will be covered, such as tasks formulation, optimization space of passes exploration, passes ordering, decision-making and software characterization approaches, benchmarks collection methodics, etc. Finally, some results of author's research group investigation in construction of modern approach for phase-ordering on the top of GCC for optimization under mixed criteria will be reported. Дата: пятница 22 декабря 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада и вспомогательная презентация со слайдами с конференции Engineering & Telecommunication — En&T-2023.)
Петр Алексеевич Лозов (Санкт-Петербургский государственный университет): Relational Solver for Java Generics Type System Аннотация: In this talk, we describe a solver for Java generics type system that was implemented using relational verifier-to-solver approach. The solver finds solutions for a system of subtyping inequations with free variables, and thus can be used to determine a concrete type satisfying a set of constraints. Also, we will discuss the relational verifier-to-solver approach, some extra-relational optimizations we used in the implementation and possible applications of the solver.
(Joint work with Dmitry Kosarev, Dmitry Ivanov and Dmitry Boulytchev.) 		Дата: пятница 15 декабря 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Иван Олегович Пыльцын (Международная лаборатория логики, лингвистики и формальной философии ВШЭ): Game semantics for First-order Modal and Temporal Logics: State of the art and perspectives Аннотация: Game semantics allows us to look at basic logical concepts from another side. This approach to logic has a long history, there are plenty of different types of games: provability games, semantic games, etc. And there is an interesting type of provability game called Mezhirov's game proposed by Iliya Mezhirov for intuitionistic logic of propositions and Grzegorczyk modal logic in 2006. Mezhirov's game semantics for intuitionistic logic is interesting because of its simplicity and strong connection with Kripke semantics and Kripke models. In this talk I will describe this game and present a possible generalization to intuitionistic logic of predicates QInt (to be more precise, to some extension of QInt). Дата: пятница 8 декабря 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Леонид А. Меркин (Факультет информатики ВШЭ, Санкт-Петербурге): Bridging the gap between the modern Computer Science and "traditional" practices in Aerospace Engineering: Our experience with teaching the "C++ for Space Ballistics" program Аннотация: Before the 1990s, Computer Science and, more generally, Information Technologies were in essence areas of Applied Mathematics, and Mathematics was universally considered the main foundation of all Engineering disciplines.
In the last 30 years the situation had changed dramatically. It is nowadays a common perception among the general public and even many students and practitioners, that Mathematics, IT and Engineering have diverged, to the extent that many IT and Engineering students view Mathematics as an "unnecessary antedeluvian burden" they are obliged to pass, whereas "in modern reality, it has been completely superceded by Data Science".
Needless to say, this perception is outright wrong and is very unfortunate. The negative impact of it is the most harmful for interdisciplinary, scientifically- and computationally-intensive interdisciplinary areas, such as Quantitave Finance or Aerospace Engineering.
In an attempt to rectify this problem, we implement online educational programs aimed at students from BS to PhD levels as well as industry practitioners, to provide an integrated and constructive hands-on approach to Applied Mathematics, Computer Science and Engineering.
In our talk wediscuss in details one of such programs, "Modern C++ for Space Ballistics and Spacecraft Control Systems" which is on-going since October this year.
Биографическая справка: Леонид А. Меркин, Doctor of Mathematics (TU Deflt, Нидерланды), профессор Факультета информатики ВШЭ в Санкт-Петербурге, эксперт с 30-летним опытом работы в области прикладной математики, компьютерных наук, C++ и систем реального времени. С записями лекций Леонида Меркина можно познакомиться на его странице в YouTube. 		Дата: пятница 1 декабря 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Дополнительно есть копия таблицы Maturity Levels of Software Process, составленной Л.А. Меркиным.)
Антон Коробейников (Access Softek Toolchains & LLVM Foundation): Back to school: teaching compiler to differentiate... programs! Аннотация: Compilers could do some sophisticated code transformations these days. While customary instrumentation, code hardening and optimization-related changes certainly might be quite sophisticated, there is certainly more that could be done. Automatic differentiation is a compiler-guided code transformation that could synthesize and evaluate the partial derivative of the function specified by a real program. The approach itself is not quite new with many implementations did exist for e.g. legacy FORTRAN code, however, recent advances in computational methods and models certainly demands modern integrated and performant solutions. In this talk I review the modern first-class implementation of automatic differentiation that is already ready for use in standard Swift toolchain. Дата: пятница 24 ноября 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Semen Yurkov (University ofLuxemburg): Compositional Analysis of Protocol Equivalence in the Applied pi-calculus using Quasi-Open Bisimilarity Аннотация: In the talk I justify that a particular equivalence notion for the applied pi-calculus called quasi-open bisimilarity is suited to security and privacy problems expressed as an equivalence problem in the following senses: (1) being a bisimilarity is a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approach to proving certain equivalence problems such as unlinkability; and (3) being the coarsest such bisimilarity congruence it can establish proofs of some privacy properties where finer equivalences fail to do so. Дата: пятница 17 ноября 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
PSSV-2023: Семинар по семантике, спецификации и верификации программ: теория и приложения Международный семинар по семантике, спецификации и верификации программ (PSSV) имеет 14-летнюю историю. Он был запущен в 2010 году, чтобы стать площадкой для сотрудничества между исследователями в области семантики, спецификации и проверки программ из Содружества Независимых Государств и международных коллег. C историей и тематикой PSSV можно познакомиться на странице семинара. Программный Комитет провел Конкурс имени В.А. Непомнящего среди авторов (возрастом до 35 лет) работ, доложенных на PSSV-23 (см. Положение о конкурсе имени В.А. Непомнящего среди работ молодых ученых, поданных на PSSV"), Лауреатом конкурса стала Дарья Наильевна Исмагилова. Даты: пятница 3 ноября и суббота 4 ноября 2023 г. С Программой и материалами (презентациями, записями, расширенными рефератами некоторых работ) семинара PSSV-2023 можно познакомиться по этой ссылке, а с содержанием и результатами первых российских студенческих соревнований по верификации программ VeHa - по этой ссылке.
Николай Вячеславович Шилов (Университет Иннополис): Введение в IMO Grand Challenge Аннотация: IMO Grand Challenge - инициатива/проект, начатый в 2019 г., направленный на разработку системы искусственного интеллекта, систематически побеждающего в Международной Математической Олимпиаде (IMO). В качестве "решателя" в данном проекте используется LEAN (Proof Assistent).В выступление носит вводный и обзорный характер. Дата: среда 25 октября 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Abdelrahman Abounegm, Violetta Sim, Nikolai Kudasov (Университет Иннополис):Impressions of the Interactions between Proof Assistants and Mathematics school Аннотация: We have recently attended a school on «Interactions between Proof Assistants and Mathematics» taking place in Regensburg from Sep 18 to Sep 29. We would like to share our impressions of the school and summarise/share a few things we learned there. Violetta will talk about homotopy type theory, her impressions of the lectures by Paige North and her work on the HoTT book formalizations in Rzk. Abdelrahman will share his understanding of the place of category theory, topology, and homotopy type theory for the present/future of maths and computer science. He will also share his impressions of mathematicians using tools for programmer (such as VS Code). Nikolai will share some progress done during the school on Rzk proof assistant and related formalisation projects. Дата: пятница 13 октября 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада Н.Д. Кудасова.)
Дмитрий Александрович Кондратьев (Институт систем информатики СО РАН):Автоматизация доказательства условий корректности программ и перспективы применения машинного обучения в данной области Выступление (в трех частях) в рамках семинара Explaineable Artificial Intellegence (XAI). Даты: среда 27 сентября, 4 и 18 октября 2023 г. Записи доступны в Telegram-группе XIA и (будут доступны) в YouTube-канале XIA
Антонина Николаевна Непейвода (Московский государственный технический университет им. Н.Э. Баумана и Институт программных систем имени А.К. Айламазяна, Переславль-Залесский): Jez Recompression Algorithm for Solving Word Equations: from Theory to Implementation Аннотация: Arthur Jez introduced his recompression algorithm for solving word equations in 2013, in terms of non-deterministic computations. For now, the algorithm remains a purely theoretical concept. We describe a natural idea of subword counting, underlying the recompression technique, and some details of the algorithm experimental implementations in the functional language Refal. Дата: четверг 7 сентября 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
По сложившейся традиции нашего семинара, при совпадении дат заседаний семинара и близких по тематике конференций и семинаров участники семинара приглашаются присоединиться к заседаниям этих конференций и семинаров. Поэтому в четверг 24 августа 2023 г. участники семинара были пригашены присоединиться онлайн к конференции Parallel Architectures & Computational Technologies (PACT) Программа PACT 24 августа 2023 г. включала следующие мероприятия: Дата: четверг 24 августа 2023 г.
Алексей Недоря: 5-й элемент. Опыт разработки и реализации языка Тривиль. Аннотация: Выступление является продолжением выступления Алексея Недори Интенсивное программирование: язык Тривиль (14 апреля 2023 г.) Дана краткая история разработки, сравнение Тривиль компиляторов (на Го и на Тривиле). Интересные особенности языка на примерах работающего кода: что хорошо и что плохо. Дата: четверг 10 августа 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Сергей Антонович Морозов (Высшая Школа Экономики СПб): Efficient and effective symbolic execution: technologies overview Аннотация: Software verification is a significant and complicated problem. Many approaches exist to resolve that problem in different ways. In our lecture, we will discuss one of them: symbolic execution. We will consider its structure and applications.
Firstly, we will consider three separate parts: path selection, memory model and solvers. For each part, we will present several ideas, which we have implemented on top of the state-of-art KLEE symbolic execution engine, including heuristics for path selection, lazy initialization mechanism to verify recursive data structures, symcretes infrastructure and their application to memory model (to maintain a representation of objects with indeterminate sizes).
Secondly, we will show how we adapted our engine to process traces from static analysers to reduce the number of false-positive verdicts. 		Дата: среда 28 июня 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Ross Horne : Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom Аннотация: Over the past couple of decades we, as a community, have been exploring behavioural properties that session types guarantee. We mainly agree that session types should guarantee deadlock-freedom; and, when there are three or more parties, better still, we target a finer property such as lock-freedom, which ensures that whenever a participant wants to do something they eventually will. Lock-freedom is more difficult to define precisely than deadlock-freedom, not least because it is sensitive to the precise notion of fairness we assume.
Recently, I made the observation that assuming a minimal realistic notion of fairness called "justness", developed by my co-authors Peter Höfner and Rob van Glabbeek, leads to a notion of lock-freedom that tightly matches session types. After investigating this observation we determined that, in fact, the resulting notion of "just lock-freedom" is complete​ for session types. This was a surprise for me and appears to be the first such completeness result for session type systems: that is, if you directly model check the behavioural property "just lock-freedom", then you can always synthesize a global type for that session. This result is surprisingly sensitive to the fine details of (1) the definition of the operational semantics of sessions, (2) the precise definition of projection from global types to local types, and (3) the precise formulation of lock-freedom, as well as (4) the fairness assumption. The design decisions we made to achieve completeness were informed by a systematic investigation where we took into account all possible notions of fairness.
(There is a 15min video introducing this problem.) 		Дата: среда 21 июня 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Совместное Совещание по языку Рефал МГТУ им. Н.Э. Баумана (кафедра ИУ9) и ИПС им. А.К. Айламазяна РАН Список выступлений:
  • Андрей Петрович Немытых (ИПС им. А.К. Айламазяна РАН) "О специализации математических формул и утверждений"
  • Александр Владимирович Коновалов (МГТУ им. Н.Э. Баумана) "Опыт использования Рефала в учебном процессе"
  • Николай Вячеславович Шилов (Университет Иннополис) "Хорошо структурированные системы помеченных переходов, их отношение к моделям интуиционистких модальных логик и к суперкомпиляции (обнаружению зацикливания программ)"
  • Антонина Николаевна Непейвода (ИПС им. А.К. Айламазяна РАН и МГТУ им. Н.Э. Баумана) "Анализ моделей в теории строк для преобразования и ускорения Рефал-программ"
  • Исмагилова Дарья (МГТУ им. Н.Э. Баумана) "Регулярные выражения с повторными переменными: обзор формализмов и алгоритмы сопоставления"
  • Камиль Яушев (МГТУ им. Н.Э. Баумана) "Распознавание группового экранирования образцов в Рефале-5λ"
  • Беликова Юлия (МГТУ им. Н.Э. Баумана) "О структуре неоднозначностей в формальных языках"
 Дата: суббота 17 июня 2023 г. Видеозапись совещания и презентации докладов любезно представлены организаторами и доступны на странице совещания.
Валентин Соболь (Санкт-Петербургский политехнический университет): KSMT: a Platform for Unified Use of SMT Solvers Аннотация: Many researchers working in the field of program verification and analysis use various SMT solvers in their tools. At the same time, they face many difficulties: different solvers have different capabilities, provide different APIs, and support different additional options. We present the developed KSMT platform, which provides a unified programming interface for accessing various SMT solvers features, allows transparent switching between solvers, and also provides additional features such as advanced work with expressions, full-featured solver launch management, etc. Дата: среда 14 июня 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
По сложившейся традиции нашего семинара, при совпадении дат заседаний семинара и Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE), участники семинара приглашаются присоединиться к заседаниям SYRCoSE. SYRCoSE организуется ежегодно начиная с 2007 широко известными специалистами в программной инженерии и программировании Александром Константиновичем Петренко (Институт системного программирования РАН, Москва) и Андреем Николаевичем Тереховым (Санкт-Петербургский Государственный Университет).

Программа Коллоквиума SYRCoSE-2023включала три пригашенных (пленарных) доклада: 		Даты: вторник 30 мая - четверг 1 июня 2023 г. Презентации приглашенных докладов (см. ссылки в колонке слева) любезно предоставлены организаторами SYRCoSE-2023.
Ольга Авенировна Невзорова (Казанский федеральный университет): Образовательная онтология ONTOMATHEDU: проблемы онтологического инжиниринга Аннотация: Доклад посвящен задачам онтологического инжиниринга в области школьного образования. На основе предложенного подхода к проектированию онтологии в области школьной математики разработана образовательная полилингвальная математическая онтология OntoMathEdu для школьного курса планиметрии. Описаны особенности организации образовательных онтологий, отражающих специфику предметного обучения в различных странах, в том числе учет методики преподавания и языка обучения. Специфические особенности организации предметной области позволяют учитывать, в том числе, и уровень подготовки обучающихся. Для решения этих задач предложена новая структура организации онтологий с образовательными проекциями, образовательными уровнями и пререквизитами. Дата: пятница 26 мая 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Николай Дмитриевич Кудасов (Университет Иннополис): Rzk Proof Assistant and Simplicial HoTT Formalisation Аннотация: Rzk is an experimental proof assistant for synthetic infinity-categories. This project has started with the idea of bringing Riehl and Shulman's 2017 to "life" by implementing a proof assistant based on their type theory with shapes. An early prototype with an online playground is available. Perhaps, the largest formalizations are available in two related projects done in collaboration with Emily Riehl and Jonathan Weinberger: https://github.com/fizruk/sHoTT and https://github.com/emilyriehl/yoneda. In this talk, I will introduce the proof assistant, demonstrate some of its features, and briefly go over available formalizations. (Early prototype of a proof assistant is available). Дата: среда 24 мая 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Алексей Валерьевич Канатов: Extreme objects Аннотация: This presentation aims to cover the approach which is based on the statement – everything is an object. That is why term object is the essential one. Set of operations on objects is fixed; object life cycle has just 3 stages; object immutability is defined. Term attribute is introduced as it is a key part of any object internal structure. Relations between objects are defined. Two atomic objects are introduced as an introduction to constant objects concept. What is class type in the object world? Brief introduction into active objects concept is given. Дата: среда 17 мая 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Сергей Александрович Гречаник: Доказательство свойств функциональных программ методом насыщения равенствами Аннотация: Был представлен обзор диссертации (2017). Цель работы — исследовать возможность применения комбинации методов насыщения равенствами и многорезультатной суперкомпиляции для выявления и доказательства свойств программ на нестрогом функциональном языке первого порядка. Настоящая работа показывает, что на основе метода насыщения равенствами и преобразований из суперкомпиляции можно построить систему преобразования функциональных программ, применимую для доказательства эквивалентности. Показано, что при этом удаётся избежать проблемы, связанной с комбинаторным взрывом количества функций, отличающихся только порядком аргументов. Также было показано, что можно сформулировать принцип индукции как специальное преобразование, работающее в рамках системы насыщения. Даты: пятница 5 и 12 мая 2023 г. Рабочая (необработанная) запись первой (5 мая) и второй (12 мая) частей доклада на YouTube-канале ИСИ СО РАН. ( Есть презентация (всего) доклада.)
Андрей Вячеславович Зыков (Университет Иннополис): Язык разработки микросхем Verilog HDL и инструменты разработки с открытым исходным кодом Аннотация: Был дан краткий обзор процесса проектирования цифровой логики с использованием языка Verilog HDL и обсуждение инструментов проектирования с открытым исходным кодом, таких как OpenLANE и OpenROAD. (По материалам статьи: Зыков А.В., Ильясов Р.Ф. "Анализ работы программных инструментов с открытым исходным кодом OpenLANE для разработки микросхем". Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС). 2022. Выпуск 4. С. 87-92. doi:10.31114/2078-7707-2022-4-87-92) Даты: среда 26 апреля и 3 мая 2023 г. Рабочая (необработанная) запись первой (23 апреля) и второй (3 мая) частей доклада на YouTube-канале ИСИ СО РАН. ( Есть презентация (всего) доклада.)
Даниил Сергеевич Степанов (Санкт-Петербургский политехнический университет): How fuzzing can help improve compiler quality Аннотация: Сompiler is a software project that automatically translates code written in one programming language into another representation, usually low-level. The importance of the reliability of such a project can not be overestimated, since mistakes in it can lead to fatal consequences. This also applies to the Kotlin compiler developed by JetBrains. This project is relatively young, with the first release in 2016. At the end of 2021, Kotlin ranked 33rd in the TIOBE ranking and is the main development language for the Android platform. Due to the popularity and youth of the language, the task of its testing is very important. Despite efforts to manually test the compiler, users encounter errors that can lead to serious consequences. In addition to manual written tests there are many automated compiler testing methods, of which fuzzing is one of the most powerful and useful. Compiler fuzzer is a tool that generates a random program in the target language and checks how the compiler works on it. In the presentation we are presenting Backend bug finder (BBF) — a platform for compiler fuzzing and the implementation on its basis of the Kotlin compiler fuzzer. Over a year and a half of work, our tool has found thousands of different compiler bugs, of which more than 200 were sent to the developers, and more than 80 have been fixed. Дата: пятница 21 апреля 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Ершовская лекция 2023 г. 19 апреля - День Рождения Андрея Петровича Ершова. По сложившейся традиции мы приглашаем участников семинара присоединиться к традиционной Ершовской лекции, организуемой Институтом систем информатики им. А.П. Ершова.
В 2023 г. лекцию прочитал директор НИВЦ МГУ и филиала МГУ в г. Сарове, член-корреспондент РАН, профессор Владимир Валентинович Воеводин, тема лекции Суперкомпьютерные технологии, параллельные вычисления и структура алгоритмов.
Аннотация: Современный компьютерный мир за последние годы сильно изменился, причем изменения коснулись всей вертикали от суперкомпьютеров, имеющих рекордную производительность, до мобильных компьютерных устройств, имеющихся сейчас в распоряжении почти каждого человека. Принципиальное технологическое изменение – это увеличение степени параллелизма, присущего компьютерам. И если число параллельно работающих процессоров в суперкомпьютерах давно измеряется многими десятками тысяч и стало обычным явлением, то параллелизм многоядерных смартфонов и планшетов многих все еще удивляет. Но привыкать к этому необходимо, потому что по-другому уже не будет, и степень параллелизма со временем будет только расти. Почему нужны и важны суперкомпьютеры? Как работать на параллельных вычислительных системах и суперкомпьютерах? Что изменится с переходом на параллельные платформы? Что сегодня нужно знать о свойствах и параллельной структуре алгоритмов? Эти и многие другие вопросы, навеянные параллелизмом в архитектуре компьютеров, были затронуты в докладе. 		Дата: среда 19 апреля 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Алексей Недоря: Интенсивное программирование: язык Тривиль Аннотация: В докладе обсуждаются первые шаги перехода от экстенсивного к (см. интенсивному программированию), а именно язык Тривиль, как первый язык проекта "Языки выходного дня". Дан краткий рассказ о целях разработки языка и его основных конструкций, предлагается использовать язык и компилятор в обучающем процессе. Дата: пятница 14 апреля 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Сергей Михайлович Старолетов (Алтайский государственный технический университет): Обзор и приложения алгебры Клини с тестами Вместо аннотации: The 2022 Alonzo Church Award for Outstanding Contributions to Logic and Computation The ACM Special Interest Group on Logic (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS) are pleased to announce that the 2022 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given to
Dexter Kozen
for his fundamental work on developing the theory and applications of Kleene Algebra with Tests, an equational system for reasoning about iterative programs, published in:
Kleene Algebra with Tests. ACM Transactions on Programming Languages and Systems 19(3): 427-443 (1997)

(см. The 2022 Alonzo Church Award) 		Дата: среда 12 апреля 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Алексей Валерьевич Канатов: Incidence matrix in OOP world Аннотация: This talk is devoted to the application of the particular graph representation for the purpose of support of multiple inheritance for methods and fields with different, close to optimal runtime support schemes for dynamic dispatch with possibility of dynamic loading of new classes. Дата: среда 5 апреля 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Евгений Александрович Зуев (Университет Иннополис): Исходный код: скрытое знание и как его показать? Аннотация: Во многих современных исследованиях утверждается, что на изучение и понимание программы уходит около 70% рабочего времени программиста, и только 5% времени занимает непосредственное написание и редактирование кода. Кроме того, отмечается, что ключевой и наиболее затратный по времени процесс разработчика в ходе создания программы — это выстраивание мысленной модели кода.
Современные программные системы характеризуются, помимо прочего, существенной и постоянно возрастающей сложностью – как в аспекте их физических размеров, так и в плане глубоких и различных по своей природе связей между их частями и компонентами.
С другой стороны, языки программирования, используемые в разработке программных систем, также весьма сложны – и синтаксически, и особенно семантически. Более того, тексты программ зачастую не отражают в явном виде всех аспектов их функционирования, и чем выше уровень языка, тем больше в нем так называемой «скрытой семантики» (hidden semantics).
Традиционно информация о программе представляется в виде документации, которая, как правило, представляет собой неформальное или полуформальное описание тех или иных особенностях, правилах ее использования и т.д. – то есть, содержит информацию о внешней стороне программы («взгляд пользователя»).
С другой стороны, аспекты внутреннего устройства программы, как на уровне ее общей архитектуры, так и на уровне отдельных компонентов (функций, классов), как правило, никак не документируется.
В то же время, именно внутреннее устройство программы, смысл (семантика) ее компонентов является критически важным – особенно для крупных долгоживущих программных комплексов, которые, как правило, эволюционируют и в процессе сопровождения подвергаются рефакторингу, добавлению новых функциональных возможностей, оптимизации и другим модификациям.
Поэтому выявление как семантики структурных компонентов программы, архитектуры системы в целом и представление (визуализация) их в форме, удобной для анализа, – является критически важной и актуальной, особенно учитывая тот факт, что в настоящее время для многих современных ЯП не существует адекватных инструментов для подобного анализа и визуализации.
Данное выступление посвящено проблеме глубокого анализа семантики программ, представленных в исходных текстах, и наглядного (удобного для восприятия) отображения знания о ее семантике. Предлагается ряд подходов и технологий, направленных на извлечение и визуализацию знаний о семантике программ, в том числе «скрытой семантики», а также общей архитектуре программных систем. 		Дата: среда 22 марта 2023 г. Есть рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН докада и обсуждения. ( Есть презентация доклада.)
Специальное заседание в Международный женский день
Special meeting in International Women's Day 		В 2023 г. семинар продолжил традицию специальных заседаний в Международный женский день (8 марта 2021 и 8 марта 2022).
Программа заседания:
  • Hamna Aslam (Иннополис Университет, Россия, и University of Toulouse, France): Affordance Theory in User Experience Evaluation
    Abstarct: Hamna Aslam presented her doctoral thesis contribution in this talk.
    The word "user experience'' encompasses the entire design area. User experience guides design decisions. It informs us which attributes of designs suit and which attributes do not support user needs. While design as a discipline is well studied, the user experience as a discipline got attention only in recent decades. The user experience, just like any scientific field of inquiry, requires systematic methods and studies to gain authentic insights into user needs and preferences. This thesis fills this gap and examines user experience under a significant theory of human actions, scientifically called the theory of affordances. The original contribution to knowledge is the development of the synthesis that, user evaluation process must be based on both Gibson and Norman's approach to affordances. Both approaches to affordances explain user interactions from cognitive and environmental dimensions. Such as affordance derived from cognitive capacities and the affordance that the environment encourages. Further, this synthesis is operationalized in a user evaluation methodology. The methodology involves identifying user affordances through focused conversation-based interviews and further evaluating on Gibson and Normans' approach to affordances. This user experience evaluation method applies to any design domain. As a result, anyone who wants to evaluate a design's desirability can utilize this method. The thesis considers different design artifacts to demonstrate the applicability of the proposed method in various contexts. The thesis asserts and proves how important it is to employ affordance theory to understand user experience. The work operationalizes this theory on various design artifacts, including games, workspace, and documentation. As a result, the thesis application extends beyond classified design domains and lays the groundwork for the discipline of user experience evaluation.
  • Антонина Николаевна Непейвода (Московский государственный технический университет им. Н.Э. Баумана и Институт программных систем имени А.К. Айламазяна, Переславль-Залесский): To transform is to understand: an experiment of building an interactive regular language converter.
    Abstract: Nowadays remote student-tutor collaboration becomes a part of academy routine, and sometimes, lacking in-person communication, it becomes challenging to retain interactivity and support any teamwork. We want to share an experience of building a joint project within the formal language BMSTU course aiming to make the automata theory concepts more tangible and increase the students' research interest in the formal languages domain. In particular, we aimed to check experimentally propositions given in the paper of Allauzen and Mohri presenting a unified сonstruction of the Glushkov, Follow, and Antimirov automata.
Дата: среда 8 марта 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН:
Дмитрий Юрьевич Булычев (Санкт-Петербургский государственный университет): Relational programming, interpreters, and program synthesis Аннотация: Relational programming is an attractive technique based on the idea of constructing programs as relations. While in general some relational effects can be reproduced with a number of languages for logic programming, such as Prolog, Mercury, or Curry, in a narrow sense relational programming amounts to writing relational specifications in miniKanren. MiniKanren, initially designed as a small relational DSL, embedded in Scheme/Racket, was later implemented for a number of general-purpose host languages, including Scala, Haskell, Standard ML and OCaml.
With relational approach, it becomes possible to give simple and elegant solutions for the problems, otherwise considered as tricky, tough, tedious, or boring. For example, relational interpreters can be used to derive quines - programs, which reduce to themselves, as well as twines or thrines (pairs or triples of programs, reducing to each other); a straightforward relational description of simply typed lambda calculus inference rules works both as type inferencer and inhabitation problem solver; relational list sorting can be used to generate all permutations, etc.
We can apply relational programming to the problem of constructing a solver for a certain search problem from its solution verifier. The main idea behind the approach we advocate is to consider a verifier as an interpreter which takes a data structure to search in as a program and a candidate solution as this program's input. As a result the interpreter returns “true” if the candidate solution satisfies all constraints and “false” otherwise. Being implemented in a relational language, a verifier becomes capable of finding a solution as well. 		Дата: среда 22 февраля 2023 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)