Метка «agda»

в 16:58, , рубрики: agda, coq, Git, github, type theory, математика, перевод, переводы, метки: , , , , , ,

Перевод статьи Андрея Бауера — The HoTT book

Книга по HoTT закончена!

Начиная с весны, и даже раньше, я участвовал в командном проекте по написанию книги по гомотопической теории типов (Homotopy Type Theory). Она наконец написана и готова к употреблению. Вы можете скачать книгу бесплатно: homotopytypetheory.org/book/. Майк Шульман рассказал о содержании книги, так что я не буду повторять то же самое. Вместо этого я бы хотел прокомментировать некоторые социо-технологические аспекты создания книги и, в частности, рассказать о том, чему нас научило сообщество Open source.
Читать полностью »

в 20:04, , рубрики: agda, haskell, Программирование, метки: ,

Доброго времени суток, уважаемый читатель!

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

в 11:53, , рубрики: agda, fprog, haskell, icfpc, Блог компании JetBrains, встреча, Программирование, функциональное программирование, метки: , , , , ,

Встреча FProg 2012 07 в Петербурге
В четверг, 12 июля 2012 года в 19:00 в петербургском офисе компании Яндекс при поддержке компании JetBrains и журнала «Практика функционального программирования» пройдёт очередная встреча FProg. Встреча состоится накануне программистского конкурса ICFP Contest 2012.

Обязательная запись на встречу для доступа в офис осуществляется на странице встречи через Twitter-аккаунт.

Темы докладов:

  • Евгений Котельников. Зависимые типы в Haskell
  • Ян Малаховски. Введение в Agda
  • Андрей Власовских. Команда spb-archlinux на ICFP Contest 2009

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

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