STEP-2024

 

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

Семинар STEP-2024 является продолжением в 2024 г. семинаров STEP-2023 (работавшего в 2023 г.) и ru-STEP (работавшего в 2020-2022 гг.)

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

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

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

Как зарегистрироваться для участия в семинаре, в обсуждениях и/или как подать заявку на выступление:

  • Желающие выступить на семинаре приглашаются написать по электронной почте любому/нескольким/всем членам Программного Комитета (с темой письма "Заявка на STEP-2024").
  • Желающие получать напоминание (оповещение) о ближайшем заседании накануне семинара (тему, докладчика, техническую среду проведения, дату и время) могут заполнить Google-форму.
  • Для обсуждения работы семинара, состоявшихся докладов и других связанных с семинаром тем создана Telegram-группа (чат).

Предстоящие заседания семинара:

Николай Дмитриевич Кудасов(Университет Иннополис): Free Foil в спокойном темпе Аннотация: Планируется 5 выступлений на три недели. Предварительно тематический план следующий:
  1. Introduction to Capture-Avoiding Substitution, Rewriting, and Higher-Order Unification. In this talk, I will explain the problems that arise when working with bound names (e.g. local variables) and their practical implications for the implementation of modern compilers, proof assistants, and theorem provers. The applications are covered superficially, to provide motivation for the next talks.
  2. (optional) De Bruijn Notation and Locally Nameless Representations. This talk focuses on several variations of "locally nameless" representations, including de Bruijn indices, the locally nameless representation of Arthur Chargueraud, de Bruijn notation as nested data types a la Bird and Paterson, generalized generalized de Bruijn notation a la Kmett, and co-de Bruijn indices of McBride.
  3. (optional) Higher-Order Abstract Syntax. This talk focuses on a family of techniques that "cheat" the problem of name binders by reusing the binders of the host language (which can be any language with support for higher-order functions). In particular, we will look at both classical HOAS and parametric HOAS (PHOAS).
  4. The Barendregt convention, the Rapier, and the Foil. In this talk, we will discuss three implementations of the Barendregt convention: a naive implementation, an efficient algorithm used in GHC and Agda, and a novel safe version of the latter, used in the implementation of the Dex programming language.
  5. Free Scoped Monads and Free Foil. We now split syntax into two its signature (specification of syntactic constructions) and the recursive structure with variables and binders (which can be handled generically). Such separation enables a kind of generic programming: it is now possible to implement certain algorithms once for (almost) any language with binders. Apart from relatively straightforward capture-avoiding substitution, we also mention the ability to implement alpha-equivalence, conversion functions, and non-trivial higher-order unification algorithms (at least in principle).
Каждая тема рассчитана примерно на 1 час доклада + 30 мин вопросы по ходу/в конце.
К сожалению, организаторы семинара вынуждены отложить серию докладов Н.Д. Кудасова (которая изначально планировалась с 4 по 20 сентября). О времени, когда состоится эта серия докладов Н.Д. Кудасова, будет объявлено дополнительно. Семинары пройдут в гибридном формате: в Университете Иннополис и в Zoom, аудитория и данные для подключения будут объявлены позже.

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

Андрей Михайлович Миронов (Московский государственный университет им. М.В. Ломоносова): Процессный подход к верификации криптографических протоколов Аннотация: В докладе изложена новая математическая модель криптографических протоколов, и приводятся примеры применения этой модели для решения задач верификации криптографических протоколов. Криптографические протоколы -- это коммуникационные протоколы, реализованные с применением криптографических алгоритмов для решения задач защиты информации, в рамках которого стороны информационного взаимодействия последовательно выполняют определенные действия и обмениваются сообщениями. Они используются, например, в электронных платежах, электронных процедурах голосования, системах доступа к конфиденциальным данным, и т.д. Ошибки в криптографических протоколах могут привести к большому ущербу, поэтому необходимо использовать математические методы для обоснования различных свойств корректности и безопасности криптографических протоколов.
В докладе изложен новый метод формальной верификации криптографических протоколов. Для моделирования криптографических протоколов в докладе вводятся понятия последовательного и распределенного процессов. Предлагаемый подход предназначен для построения формальных доказательств корректности для заведомо корректных криптографических протоколов. Особенностью модели протоколов является её простота по сравнению с другими моделями протоколов, основанных на логических формулах или на алгебраических процессных выражениях. Участники протоколов представляются в виде графов, представляющих системы переходов. Действия, выполняемые участниками, являются метками этих переходов. Методы обоснования корректности протоколов, рассматриваемые в настоящей статье, связаны с рассуждениями для графов, которые более просты и наглядны по сравнению с методами, основанными на построении логического вывода в логических и алгебраических моделях протоколов.
Дата: пятница 11 октября 2024 г. Есть презентация доклада.
Антонина Николаевна Непейвода (Московский государственный технический университет им. Н. Э. Баумана): Обзор выразительных возможностей формальных языков с захватом в память Аннотация: В докладе рассмотрены два класса языков, привлекшие значительный интерес исследователей в XXI веке: языки расширенных регулярных выражений и языки уравнений в словах. Будет приведён обзор существующих результатов о выразительных возможностях данных классов языков, а также обсуждение их взаимосвязи. Дата: пятница 27 сентября 2024 г. Рабочая (необработанная) запись на RuTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Евгений Сергеевич Муравьев (Университет Иннополис): Краткий обзор дистрибутивов Linux Аннотация: В канун День Рождения Linux (одного из четырех) был дан краткий обзор истории и архитектуры (а также личные впечатления) дистрибутивов Linux, с которыми есть опыт работы. Дата: пятница 13 сентября 2024 г. Рабочая (необработанная) запись на YouTube-канале и на RuTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Сергей Михайлович Старолетов(Алтайский государственный технический университет): Классификация коммитов в git репозиториях для поиска наиболее частых исправлений ошибок в системном программном обеспечении (ядро Linux и проекты кибефизических систем) Аннотация: В средах системного программного обеспечения циркулирует огромное количество информации, поэтому крайне важно использовать эту информацию для улучшения их работы. Одной из таких систем является ядро Linux, которое не только поставляется с полностью открытым исходным кодом, но и предоставляет исчерпывающую историю о разработке в своем git-репозитории. Вычисляя расстояния между сообщениями об исправлении ошибок, превращая их в вектора и группируя в кластеры, мы далее можем эффективно классифицировать и выявлять наиболее часто возникающие ошибки. Наш подход применяется к нескольким важным частям ядра Linux, что позволяет понять, что происходит с ошибками в различных его подсистемах. В результате мы показываем сводку исправлений ошибок в таких частях ядра Linux, как kernel, sched, mm, net, irq, x86 и Arm64.
Киберфизические системы представляют собой симбиоз многоуровневых систем управления и учитывают физические аспекты функционирования целевых объектов. Ошибки в таких системах могут быть связаны как с неправильной организацией кода и работой аппаратных средств, так и с неверным пониманием физических законов и их численной аппроксимацией. Продолжая предыдущую работу, мы применяем технологии автоматизированного анализа коммитов в git-репозиториях некоторых известных киберфизических систем с последующей классификацией собранных сообщений о фиксации изменений, написанных разработчиками таких систем. В работе мы обсуждаем выявленные сильные ключевые слова и обобщенные сообщения об исправлениях, которые способны показать основные классы ошибок в этих проектах.
Публикации по теме:
  • Analyzing hot bugs in the Linux kernel by clustering fixing commit messages (Труды института системного программирования РАН, 2023, том 35, выпуск 3, страницы 215–242, DOI: https://doi.org/10.15514/ISPRAS-2023-35(3)-16
  • Exploring the Taxonomy of Commits in Cyber-Physical Systems for Enhanced Error Fixes Investigation (Труды института системного программирования РАН, 2024, том 36, выпуск 2, страницы 33–46, DOI: https://doi.org/10.15514/ISPRAS-2024-36(2)-3
Дата: среда 21 августа 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Алексей Недоря: Архитектурное программирование. Языки Арс и Арвиль Аннотация: Архитектурное программирование (АРП) - это технология, обеспечивающая корректность описания архитектуры программной системы в течении всего времени жизни системы. Описание архитектуры состоит из описания устройства системы, описание частей (компонент) и их взаимодействия. В АРП описание архитектуры делается с помощью формальной нотации и является входным данным для компиляторов и/или систем сборки. Для практической проверки жизнеспособности технологии разрабатываются два экспериментальных языка: Арс - описание системы и Арвиль - разработка компонент. Дата: среда 3 июдя 2024 г. Есть рабочие записи на YouTube-канале ИСИ СО РАН первой и второй частей доклада. ( Есть презентация доклада.)
Артем Сергеевич Бурмяков (Университет Иннополис): Towards a Tractable Exact Test for Global Multiprocessor Fixed Priority Scheduling Аннотация: An exact schedulability analysis of a system of sporadic tasks to be executed upon a multiprocessor platform is proved to be a weakly NP-hard computational problem. The available exact tests suffer from a high computation time and memory requirement, which make them intractable for large realistic real-time systems. On the other hand, the available approximate sufficient tests, which are faster and consume less memory, are very pessimistic in provisioning the execution requirements of a given system. Motivated by these observations, we propose an exact schedulability test for constrained-deadline sporadic tasks under global multiprocessor fixed-priority scheduler (GFP), which is significantly faster and consumes less memory, compared to any other available exact test. To derive a faster test, we exploit the idea of a state-space pruning, aiming at reducing the number of feasible system states to be examined by the test. The resulted test is multiple orders of magnitude faster with respect to other state-of-the-art exact tests. The C++ implementation of our test is publicly available. Даты: первая часть - среда 6 марта, вторая часть - среда 22 мая, заключительная третья часть - среда 26 июня 2024 г. Есть рабочие записи на YouTube-канале ИСИ СО РАН первой, второй и третьей частей доклада, а также презентация доклада. ( Есть презентация доклада.)
Николай Вячеславович Шилов (Университет Иннополис): "Теория всего": унификация паттернов дизайна алгоритмов (метода отката, ветвей и границ, жадных алгоритмов, метода разделяй и властвуй, и динамического программирования...) Аннотация: Курс проектирования и анализа алгоритмов является обязательной составляющей учебных программ по информатике всех уровней. В университетах этот курс обязательно включает изучение структур данных, методы проектирования алгоритмов, теорию сложности и т.д. Этот курс знакомит с такими методами проектирования алгоритмов, как жадные алгоритмы, динамическое программирование, метод разделяй и властвуй, метод отката, метод ветвей и границ. Обычно знакомство с этими методами происходит на примерах. Но они могут быть (полу)формализованы в виде рекурсивных "паттернов" (с использованием map и reduce), специфицированы условиями частичной и/или тотальной корректности и обоснованы (доказаны) методом Флойда верификации алгоритмов. Даты: первая часть - среда 22 мая, вторая (заключительная) часть - среда 19 июня 2024 г. Рабочие (необработанные) записи на YouTube-канале ИСИ СО РАН первой и второй частей доклада. ( Есть презентация доклада.)
Александр Иванович Легалов (Высшая школа экономики, Москва): Процедурно-параметрический полиморфизм и его интеграция с языком программирования C Аннотация: Разработка больших программ часто связана с инкрементальным расширением уже написанного кода. При этом встречаются ситуации, когда альтернативные программные объекты формируются во время выполнения. В этом случае для их идентификации и последующей обработки используется либо явная проверка типа, либо один из методов динамического полиморфизма, предоставляемый тем или иным языком программирования. Расширение программы за счет новых альтернатив, добавляемых в ходе разработки, может привести к модификации уже написанного кода. В этих случаях для минимизации изменений вместо явной проверки типов обычно применяются методы динамического полиморфизма. Из них к широко известным можно отнести ОО полиморфизм, использование интерфейсов в Go и типажей в Rust. Процедурно-параметрический полиморфизм является альтернативным подходом. Рассматриваются его особенности и интеграция с языком программирования C. Представлены дополнительные синтаксические конструкции, ориентированные на поддержку подхода, их возможности и варианты реализации. Приводятся примеры эволюционного расширения кода для простых ситуаций демонстрирующие большую гибкость по сравнению с существующими подходами. Также рассматривается моделирование паттернов проектирования, повышение надежности за счет обертки над ненадежными языковыми конструкциями языка C. Дата: среда 29 мая 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
По сложившейся традиции нашего семинара участники семинара приглашаются присоединиться к заседаниям Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE). SYRCoSE организуется ежегодно начиная с 2007 широко известными специалистами в программной инженерии и программировании Александром Константиновичем Петренко (Институт системного программирования РАН, Москва) и Андреем Николаевичем Тереховым (Санкт-Петербургский Государственный Университет).

Программа Коллоквиума SYRCoSE-2023 включала два пригашенных (пленарных) доклада:
  • Konstantin Sorokin (ISP RAS): AI-driven Software Engineering: Overview, Advancements and Challenges
  • Vladimir Itsykson (ITMO University): Formal Library Specifications: Application in the Tasks of Integration, Analysis and Synthesis of Programs
Даты: среда 29 мая - четверг 30 мая 2024 г. Презентации приглашенных докладов будут доступны позже.
Евгений Александрович Зуев (Университет Иннополис): Modelling C++ inheritance and dynamic semantics using a C++ virtual machine Аннотация: Доклад представляет экспериментальный программный стенд, предназначенный для моделирования ключевых свойств языка С++, включая механизмы наследования (единичного, множественного и виртуального) и полиморфизма. Стенд включает компилятор представительного подмножества языка С++ в низкоуровневый интерпретируемый язык IML и виртуальную машину, реализующую аспекты динамической семантики С++ в части полиморфизма (виртуальные функции с перекрытиями, динамическое приведение типов) и распределения динамической памяти. Стенд может использоваться как инструмент моделирования различных программных конфигураций для оценки эффективности применения моделируемых свойств С++. Проект выполняется группой студентов университета Иннополис под руководством автора доклада. Дата: среда 8 мая 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.)
Ершовская лекция 2024 г. 19 апреля - День Рождения Андрея Петровича Ершова. По сложившейся традиции мы приглашаем участников семинара присоединиться к традиционной Ершовской лекции, организуемой Институтом систем информатики им. А.П. Ершова.
В 2024 г. лекцию прочитал член Правления ключевых ИТ-ассоциаций России – АПКИТ и Руссофт Владимир Васильевич Рубанов, тема лекции Риски и преимущества открытости исходных кодов вашего программного обеспечения.
Аннотация: В докладе рассмотрен феномен открытого исходного кода (open-source) программных проектов. Будет представлен анализ основных движущих сил и типов участников открытых проектов. Приведены примеры важных проектов и участия различных компаний в их разработке. Центральное место доклада занимает анализ преимуществ и рисков, которые возникают в связи с открытием исходного кода того или иного продукта или компонента. Показано наличие оптимальной точки открытия кода (в плане момента времени и объема открытия) в зависимости от ситуации. Отклонение от такой точки для конкретного проекта приводит либо к "недооткрытию" (under-open-sourcing), либо к "переоткрытию" (over-open-sourcing), что непосредственно влияет на развитие продукта. Наконец, в докладе будет рассмотрена история участия в проектах с открытым кодом компании Huawei, которая из состояния отрицания необходимости открытия кода за считаные годы превратилась в одного из мировых лидеров open-source движения.
Дата: четверг 18 апреля 2024 г. Есть запись лекции на YouTube-канале ИСИ СО РАН.
Андрей Валентинович Климов (Институт прикладной математики им. М.В. Келдыша РАН, Москва): Научное наследие В.Ф. Турчина и его кибернетические основания математики Аннотация: Научно-философское наследие Валентина Федоровича Турчина (14.02.1931–07.04.2010) состоит из трех частей:
(1) философской, объясняющей его эволюционную концепцию с центральным понятием метасистемного перехода как кванта эволюции, — книга "Феномен науки: Кибернетический подход к эволюции" [1977 (англ.), 1993, 2003 (рус.)];
(2) социальной: обсуждение эволюции общества и человека — книга "Инерция страха: Социализм и тоталитаризм" [1977];
(3) научной: суперкомпиляция в программировании и кибернетические основания математики — статья "A constructive interpretation of the full set theory" [1987] и отчеты "The Cybernetic Foundation of Mathematics" [1983].
В докладе кратко охарактеризованы первые части, суперкомпиляция опущена и дано введение в кибернетические основания математики — потенциалистской интерпретации, являющейся расширением алгоритмического конструктивизма А.А. Маркова и Э. Бишопа путем введения (модели) математика в теорию — таким образом, что удалась конструктивная интерпретация теории множеств ZF.
Дата: среда 10 апреля 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Александр Валентинович Когтенков: Объектно-ориентированное программирование без встроенных типов Аннотация: Насколько оправдано упрощение объектно-ориентированного языка программирования при доказательстве каких-то его свойств? Что можно написать на ОО языке без встроенных типов, арифметических операторов, операторов сравнения, условных инструкций и инструкций цикла? Теоретически возможность объявлять классы, переменные и процедуры, а также создавать и присваивать объекты, обращаться к переменным и вызывать процедуры должно хватить, чтобы реализовать любую программу. Но как это выглядит на практике? На семинаре будет разобран код простого примера, отвечающего на этот вопрос.
Несмотря на фундаментальную природу, работа не носит научного характера, доступна широкому кругу специалистов профильных специальностей, может быть интересна разработчикам и исследователям языков программирования и трансляторов.
Дата: среда 3 апреля 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Алексей Юрьевич Зубарев (Институт систем информатики СО РАН, Новосибирск): Взаимосвязи семантик и эквивалентностей непрерывно-временных сетей Петри со слабой временной стратегией Аннотация: Непрерывно-временные сети Петри — это расширение сетей Петри, в которых каждому переходу ставятся в соответствие временной интервал его срабатывания и локальные часы. Данная модель позволяет учитывать как функциональные (качественные), так и реально-временные (количественные) свойства моделируемых систем. Рассматриваются непрерывно-временные сети Петри со слабой временной стратегией, где ход модельного времени не форсирует срабатывания сетевых переходов. Для данной модели и ее модификаций разрабатываются и исследуются семантические представления и поведенческие эквивалентности в дихотомиях «интерливинг-частичный порядок» и «линейное-ветвящееся время». Кроме того, в контексте «слабых» непрерывно-временных сетей Петри предлагается метод редукции пространства состояний за счёт их дискретизации. Дата: среда 20 марта 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Маргарита Владимировна Коровина (Институт систем информатики СО РАН, Новосибирск): Automated Reasoning with Continuous Data Семинар STEP-2024 продолжает традицию специальных заседаний в Международный женский день: ru-STEP-2021, ru-STEP-2022 и STEP-2023.
Аннотация доклада In this talk we report on ongoing research on solving non-linear constraints over the reals occurring in a wide range of applications, starting with program verification, ranging over verification of real-world designs all the way to automation of formally verified proofs of mathematical statements.
In our framework methods from Computable Analysis and Automated Reasoning are combined to meet efficiency and expressiveness. This approach is applicable to a large number of constraints involving computable non-linear functions, piecewise polynomial splines, transcendental functions and solutions of polynomial differential equations.
We give an introduction to the ksmt calculus for checking satisfiability of non-linear constraints in a CDCL style way inspired by advances in SAT solving. Along proof search ksmt resolves two types of conflicts: linear and non-linear. Linear conflicts are delegated to a decision procedure for linear real arithmetic and non-linear conflicts are resolved by local linearisations separating the solution set and the current conflict. We show that the ksmt calculus is a σ-complete decision procedure for bounded problems.
Дата: среда 28 февраля 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН.
Всеслав Станиславович Секорин (Тверской государственный университет): Выразительные возможности операторов частичной неподвижной точки для конечных и бесконечных систем Аннотация: В работе рассмотрены различные семантики частичной фиксированной точки для конечных и бесконечных алгебраических систем. В частности, показано, что операторы частичной фиксированной точки рассматриваемых семантик можно промоделировать оператором инфляционной фиксированной точки в тех алгебраических системах, в которых есть строгий частичный порядок со сколь угодно длинными цепями. Также, например, показано что элиминировать оператор частичной фиксированной точки можно только в тех теориях, в которых любой такой оператор зацикливается за конечное число шагов. Доклад представляет материалы и результаты кандидатской диссертации на соискание ученой степени кандидата физико-математических наук по специальности 1.1.5. "Математическая логика, алгебра, теория чисел и дискретная математика". Дата: среда 28 февраля 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Игорь Сергеевич Ануреев (Институт систем информатики СО РАН, Новосибирск): Логика распознавания последовательностей состояний SSRL (State Sequences Recognition Logic) и примеры её применения для формализации темпоральных требований к управляющим программ Аннотация: Предлагается формализм для описания свойств последовательностей состояний, порождаемых системой переходов (state transition system). Этот формализм под рабочим названием SSRL (State Sequences Recognition Logic) позволяет задавать свойства поведения системы переходов, определяемого как множество последовательностей состояний, порождаемых отношением перехода. В отличие от LTL, он поддерживает императивные вставки, позволяющие сохранять информацию в именованных компонентах состояний (аналог let в функциональных языках программирования), называемых атрибутами. В тоже время он имеет более простую систему модальностей и более жесткий порядок их комбинирования по сравнению с LTL. Даются методология и примеры его применения для формализации темпоральных требований к управляющим программ, на которые он, в первую очередь, ориентирован. Цель разработки формализма применительно к решению этой задачи - расширить область применимости ранее представленного на семинаре формализма EDTL (Event-Driven Temporal Logic), который позиционируется как язык описания темпоральных требований, ориентированный на инженеров. В качестве обоснования большей выразительной силы нового формализма рассматриваются примеры требований, невыразимых на EDTL, а также определяется формальная семантика EDTL на SSRL. Дата: среда 14 февраля 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Алексей Недоря: О "граблях" в инициализации объектов в современных языках программирования Аннотация: Рассмотрены инициализации объектов в современных языках программирования Swift/Kotlin/Тривиль. (Выступление в рамках темы "филология программирования", поднятой А.В. Коноваловым во время "Дня Проблем 2023", про язык Тривиль см. выступления Алексей Недори "Опыт разработки и реализации языка Тривиль" и "Интенсивное программирование: язык Тривиль" на семинаре STEP-2023.) Дата: пятница 2 февраля 2024 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Заседание семинара посвященное Всемирному Дню Логики (https://en.wikipedia.org/wiki/World_Logic_Day) В 2024 г. мы продолжили традицию семинара (см. Logic Day 2023, Logic Day 2022 и Logic Day 2021) совместных заседаний с Математическим Клубом Университета Иннополис (см. Telegram-беседу Logic Day in Innopolis ). А так как Всемирный День Логики установлен UNESCO (United Nations Educational, Scientific and Cultural Organization), то у нас были сообщения по спектру тем Education, Science, Culture…
  1. Владик Крейнович (University of Texas at El Paso): How to Work? How to Study? Shall We Cram for the Exams? And How Is This Related to Life on Earth?
  2. Рустам Лукманов (Университет Иннополис) представит короткое сообщение об использовании нейронных сетей для решения задач с математических олимпиад
  3. Валентин А. Бажанов (Ульяновский Университет): Восстание против Аристотеля — Н.А. Васильев: жизнь и путь к "воображаемой логике"
  4. Иван О. Пыльцын (Международная лаборатория логики, лингвистики и формальной философии ВШЭ): Кратко о сильной эквивалентности арифметики Пеано и теории конечных множеств
  5. (11:30-12:30) Леонид Меркин (ВШЭ Петербург): Логика и методология математического моделирования финансовых процессов
Обычно мы выбираем дату так, что бы не конкурировать с другими событиями в честь Всемирного Дня Логики. Наш встреча состоялась вечером в пятницу 26 января и утром в субботу 27 января. Ссылки на презентацию доклада В. Крйновича и на записи выступлений И.О. Пыльцына и Л. Меркина даны в колонке слева.