Рубрика «Блог компании Образовательные проекты JetBrains» - 2

в 11:53, , рубрики: c++, cs центр, haskell, java, stepik, Алгоритмы, Блог компании Образовательные проекты JetBrains, математика, Программирование, Учебный процесс в IT

14 ноября CS центр в третий раз запускает онлайн-программы «Алгоритмы и эффективные вычисления», «Математика для разработчиков» и «Разработка на C++, Java и Haskell». Они созданы, чтобы помочь погрузиться в новую область и заложить фундамент для обучения и работы в IT.

Чтобы поступить, вам нужно будет погрузиться в атмосферу обучения и сдать вступительный экзамен. Подробнее о программе, экзамене и стоимости читайте на code.stepik.org.

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

image
Читать полностью »

в 17:36, , рубрики: jetbrains research, Блог компании Образовательные проекты JetBrains, Программирование, языки программирования

В первой части статьи про язык 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) : Prop 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, скажем, что хвост упорядоченного списка сам является упорядоченным списком (это свойство пригодится нам в дальнейшем).
Читать полностью »

в 11:28, , рубрики: Блог компании Образовательные проекты JetBrains, Программирование, языки программирования

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

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

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

в 15:12, , рубрики: c++, Блог компании Образовательные проекты JetBrains, видеолекции, курсы, Программирование

Computer Science Center — это совместная инициатива Computer Science клуба при ПОМИ РАН, компании JetBrains и Школы анализа данных Яндекса.

Центр существует, чтобы дать возможность талантливым студентам и выпускникам развиваться в интересных им направлениях: Computer Science, Data Science или Software Engineering.

Курс по C ++ в двух частях в центре читает Валерий Михайлович Лесин, valery-l, преподаватель ИТМО и CS центра, технический директор Simlabs.

Первая часть курса нужна, чтобы нарастить базу по С++: к концу семестра студенты с большой вероятностью получат достаточно навыков программирования на этом языке для решения своих задач. Пока без move semantics, sfinae, но для начала этого, скорее всего, будет достаточно.

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

Приятного просмотра!
Читать полностью »

в 9:59, , рубрики: jetbrains research, Блог компании Образовательные проекты JetBrains, образование, Учебный процесс в IT

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

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

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

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

12
Главная   |  Архив новостей  |   Android  |   Google  |   Apple  |   Microsoft  |   Информационная безопасность  |   Веб – разработка
Публикации RSS  |  Комментарии RSS
https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js