Об авторе. Антон Подкопаев является постдоком в MPI-SWS, руководителем группы слабых моделей памяти в лаборатории языковых инструментов JetBrains Research и преподавателем в Computer Science Center. За время аспирантуры он побывал на стажировках в IMDEA Software Institute (Мадрид, Испания) и в MPI-SWS (Кайзерслаутерн, Германия).

В этой статье я расскажу про научные стажировки и попробую ответить на базовые вопросы о них на основе своего опыта. Важно отметить, что эта публикация посвящена именно научным стажировкам, а не индустриальным. Последние имеют свою специфику, которая здесь не рассматривается. Более того, я никоим образом не претендую на полноту изложения: статья написана с точки зрения человека, занимающегося исследованиями в Computer Science (конкретнее — формальными аспектами языков программирования) и имеющего опыт именно таких стажировок. Тем не менее многое, описанное здесь, будет верно и для других областей.

Об авторе статьи

Александра Малышева — выпускница бакалавриата по направлению «Прикладная математика и информатика» Санкт-Петербургского Академического университета и выпускница магистратуры питерской Вышки по направлению «Программирование и анализ данных». Кроме того, исследовательница в лаборатории «Агентные системы и обучение с подкреплением» JetBrains Research, а также ассистентка преподавателя по обучению с подкреплением в бакалавриате Вышки.

Мотивация проекта

Довольно часто современные технологии используются для создания более интересных игр или красивых виртуальных миров. Однако прогресс в технических науках можно использовать в медицине. Например, сейчас разработка протезов является очень дорогой, поскольку требуется перебор большого количества различных конструкций. При этом для тестирования созданого протеза необходимо привлекать реальных людей, потому что на данный момент взаимодействие человека с протезами недостаточно исследовано.

В 2017 году в Стэнфордском университете ученые реализовали компьютерные симуляции опорно-двигательного аппарата человека, чтобы предсказывать, как человек адаптируется к конкретной конструкции протеза, и иметь возможность тестировать каждую конкретную конструкцию виртуально за считаные секунды. Когда в Стэнфорде команда физиков и биологов разработала точную модель опорно-двигательного аппарата человека с точки зрения физики и биомеханики, осталось написать алгоритм, который мог бы контролировать эту систему способом, похожим на управление человеком.

Многим знакома гипотеза зарождения человечества в Африке. В рамках этой гипотезы предполагается, что все современное неафриканское население Земли в значительной степени происходит от популяций Homo sapiens, покинувших Африку. Первым эту теорию предложил Чарльз Дарвин, основываясь на том, что человек очень близок к таким обезьянам, как гориллы и шимпанзе, которые обитают в Африке. И если в основных моментах этой гипотезы ученые уже пришли к консенсусу, то многие детали остаются дискуссионными: был ли один выход из Африки или несколько, когда это происходило, какой длительности были эти волны и так далее.

В идеале, для ответа на эти вопросы подошел бы сравнительный анализ геномов людей, проживавших в разные периоды истории — это позволило бы установить взаимосвязи между человеческими популяциями, населяющими разные территории в разные промежутки времени. Такие геномы можно выделить, например, из археологических останков, но, к сожалению, количество и качество таких геномов довольно ограничено. С другой стороны, оказывается, что часть ответа заключена в геномах современных людей. Как именно по таким геномным данным можно восстановить детали популяционной истории, мы и расскажем в этой статье.

Привет, Хабр! Сегодня мы хотим рассказать, чем занимается лаборатория методов ядерно-физических экспериментов, входящая в JetBrains Research.

Где JetBrains и где ядерная физика, спросите вы. Мы сошлись на почве любви к Kotlin, хотя в данном посте о нем речи не пойдет. Наша группа ориентируется на развитие методик анализа данных, моделирования и написание софта для ученых, и поэтому ориентирована на сотрудничество и обмен знаниями с IT-компаниями.

В этой статье мы хотим поговорить о популяризуемом нами методе статистической регуляризации, предложенном В.Ф.Турчиным в 70-х годах XX века, и его реализации в виде кода на Python и Julia.

Каждый год Институт биоинформатики в Санкт-Петербурге и Москве набирает биологов, математиков и программистов, чтобы погрузить в мир биоинформатики. Биологи учатся программировать и тренируются реализовывать идеи в коде, а информатики изучают биологию и применяют алгоритмические подходы к биологическим и медицинским задачам. Самая важная часть обучения — реальные научные проекты. В этой статье мы расскажем о работе и результатах студентов Института, сделанной под руководством Олега Шпынова из JetBrains Research в 2019 году. Проект посвящен изучению изменения хроматина человека с помощью машинного обучения.


Студенты-информатики 2019 Института биоинформатики

Это перевод статьи An introduction to context-oriented programming in Kotlin

В этой статье я постараюсь описать новое явление, которое возникло как побочный результат стремительного развития языка Kotlin. Речь идет о новом подходе к проектированию архитектуры приложений и библиотек, который я буду называть контекстно-ориентированным программированием.

Несколько слов о разрешении функций

Как хорошо известно, существует три основных парадигмы программирования (примечание Педанта: есть и другие парадигмы):

• Процедурное программирование
• Объектно-ориентированное программирование
• Функциональное программирование

В этой статье мы поговорим о функциональных зависимостях в базах данных — что это такое, где применяются и какие алгоритмы существуют для их поиска.

Рассматривать функциональные зависимости мы будем в контексте реляционных баз данных. Если говорить совсем грубо, то в таких базах данных информациях хранится в виде таблиц. Далее мы используем приближенные понятия, которые в строгой реляционной теории не являются взаимозаменяемыми: саму таблицу будем называть отношением, столбцы — атрибутами (их множество — схемой отношения), а набор значений строки на подмножестве атрибутов — кортежем.

В первой части статьи про язык Arend мы рассматривали простейшие индуктивные типы, рекурсивные функции, классы и множества.

2. Сортировка списков в Arend

2.1 Упорядоченные списки в Arend

Определим тип упорядоченных списков как пару, состоящую из списка и доказательства его упорядоченности. Как мы уже говорили, в Arend зависимые пары определяются при помощи ключевого слова \Sigma. Определение типа Sorted дадим через сопоставление с образцом, вдохновившись определением из уже упомянутой статьи про упорядоченные списки.

\func SortedList (O : LinearOrder.Dec) => \Sigma (l : List O) (Sorted l)

\data Sorted {A : LinearOrder.Dec} (xs : List A) \elim xs
 | nil => nilSorted
 | :-: x nil => singletonSorted
 | :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs))

Обратите внимание: Arend сумел автоматически вывести, что тип Sorted содержится во вселенной \Prop. Это произошло потому, что все три образца в определении Sorted являются взаимно исключающими, а конструктор consSorted имеет два параметра, оба из которых принадлежат \Prop.
Докажем какое-нибудь очевидное свойство предиката Sorted, скажем, что хвост упорядоченного списка сам является упорядоченным списком (это свойство пригодится нам в дальнейшем).

В данном посте мы поговорим о только что выпущенном JetBrains языке с зависимыми типами Arend (язык назван в честь Аренда Гейтинга). Этот язык разрабатывался JetBrains Research на протяжении последних нескольких лет. И хотя репозитории уже год назад были выложены в открытый доступ на github.com/JetBrains, полноценный релиз Arend случился лишь в июле этого года.

Мы попробуем рассказать, чем Arend отличается от существующих систем формализованной математики, основанных на зависимых типах, и о том, какая функциональность уже сейчас доступна его пользователям. Мы предполагаем, что читатель настоящей статьи в целом знаком с зависимыми типами и слышал хотя бы про один из языков, основанных на зависимых типах: Agda, Idris, Coq или Lean. При этом мы не рассчитываем, что читатель владеет зависимыми типами на продвинутом уровне.

Для простоты и конкретности наш рассказ об Arend и гомотопических типах будет сопровождаться реализацией на Arend простейшего алгоритма сортировки списков — даже на этом примере можно почувствовать отличие Arend от Agda и Coq. На Хабре уже есть ряд статей, посвященных зависимым типам. Скажем, про реализацию сортировки списков методом QuickSort на Agda есть вот такая статья. Мы будем реализовывать более простой алгоритм сортировки вставками. При этом основное внимание уделим конструкциям языка Arend, а не самому алгоритму сортировки.

В мире инженерного образования существует много отличных курсов, но зачастую программа обучения, построенная на них, обладает одним серьезным недостатком — отсутствием хорошей связности между различными темами. Можно возразить: как же так?

Когда формируется программа обучения, для каждого курса указываются пререквизиты и четкий порядок, в котором надо изучать дисциплины. К примеру, для того чтобы собрать и запрограммировать примитивного мобильного робота, нужно знать немного механики для создания его физической конструкции; основы электричества на уровне законов Ома/Кирхгофа, представления цифровых и аналоговых сигналов; операции с векторами и матрицами для того, чтобы описать системы координат и перемещения робота в пространстве; основы программирования на уровне представления данных, простейших алгоритмов и конструкций передачи управления и т.п. для описания поведения.

Есть ли все это в университетских курсах? Конечно есть. Однако к законам Ома/Кирхгофа мы получаем термодинамику и теорию поля; помимо операций с матрицами и векторами приходится разбираться с Жордановыми формами; в программировании изучать полиморфизм — темы, которые не всегда нужны для решения простой практической задачи.

Университетское обучение экстенсивно — учащийся идет широким фронтом и зачастую не видит смысла и практической значимости знаний, которые получает. Мы решили перевернуть парадигму университетского обучения STEM (от слов Science, Technology, Engineering, Math) и сделать такую программу, которая опирается на связность знаний, допуская наращивание полноты в будущем, то есть подразумевает интенсивное освоение предметов.