14 декабря в московском офисе Яндекса пройдёт ruBSD 2013 — первая российская техническая конференция по операционным системам семейства BSD. Она предназначена для системных администраторов и программистов.

На этой конференции с докладом выступит Тео де Раадт — основатель и бессменный лидер проекта OpenBSD.

С программой конференции можно ознакомиться на странице встречи.

Участие бесплатное. Необходима предварительная регистрация. Количество мест ограничено.

>>> Подробности

Увидела свет финальная версия книги «Real World OCaml». Этот учебник познакомит вас с инструментами и методами, с помощью которых можно эффективно решать разнообразные практические задачи.

В процессе чтения этой книги вы

• изучите основы языка OCaml (функции высшего порядка, алгебраические типы данных и т.п.);
• узнаете о продвинутых возможностях (функторы, первоклассные модули, объекты);
• научитесь решать практические задачи от разбора аргументов командной строки до асинхронного сетевого программирования.

Купить бумажную или электронную копию книги «Real World OCaml» можно на Amazon.com.

Электронная версия книги, распространяемая на условиях лицензии CC-BY-ND, доступна на сайте realworldocaml.org. Для получения доступа необходим аккаунт на github.

>>> Подробности

25 октября в Санкт-Петербурге состоится очередная встреча функциональных программистов.

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

• Обзор Clojure. Доклад рассматривает Clojure с практической точки зрения: основы синтаксиса, нужные утилиты и библиотеки, подводные камни. Предварительное знание Clojure не требуется.
• Зачем нужны зависимые типы. В докладе будут рассмотрены теоретические аспекты систем зависимых типов на примере системы Мартина-Лёфа. Также будут даны примеры использования зависимых типов: изоморфизм Карри-Ховарда, вычисления во время компиляции, инварианты, проверяемые во время компиляции, безопасный printf.

Участие бесплатное. Необходима предварительная регистрация.

>>> Подробности

30 октября в Москве состоится неформальная встреча Haskell-программистов для общения и обмена опытом.

На встрече будут представлены два доклада:

• Web-crawler для дискуссий в расширенных RSS-агрегаторах.
• Динамика и статика — метрики графов социальных сетей.

Участие бесплатное, но зарегистрироваться необходимо.

30 октября, в среду, с 18:30 ждем участников по адресу: Москва, ул. Льва Толстого 16, офис Яндекса, зал Экстрополис.

>>> Подробности

С 28 сентября Джон Харрисон прочитает серию лекций об автоматическом доказательстве теорем:

• Background, history and propositional logic.
• First-order logic with and without equality.
• Decidable problems in logic and algebra.
• Interactive theorem proving and proof-checking.
• Applications to mathematics and computer verification.

Лекции будут проходить в ПОМИ РАН (Санкт-Петербург, наб. р. Фонтанки, 27), Мраморный зал, второй этаж.

Слайды, видеозаписи и другие материалы лекций будут доступны для всех желающих на странице курса.

Клуб открыт абсолютно для всех: вход свободный, лекции бесплатные, никакой предварительной регистрации не требуется.

Профессор Харрисон занимается формальной верификацией в компании Intel Corporation. Его основной специализацией является верификация алгоритмов, работающих с числами с плавающей точкой.

>>> Подробности

Доступны слайды и видеозаписи лекций некоего Conor McBride.

Dependently typed functional programming languages such as Agda are capable of expressing very precise types for data. When those data themselves encode types, we gain a powerful mechanism for abstracting generic operations over carefully circumscribed universes. This course will begin with a rapid depedently-typed programming primer in Agda, then explore techniques for and consequences of universe constructions. Of central importance are the “pattern functors” which determine the node structure of inductive and coinductive datatypes. We shall consider syntactic presentations of these functors (allowing operations as useful as symbolic differentiation), and relate them to the more uniform abstract notion of “container”. We shall expose the double-life containers lead as “interaction structures” describing systems of effects. Later, we step up to functors over universes, acquiring the power of inductive-recursive definitions, and we use that power to build universes of dependent types.

http://lambda-the-ultimate.org/node/4804

С 4 ноября 2013 года на курсере начнется сабжевый курс, который продлится 7 недель (пруф).

Содержание курса:

• Week 1: Review of Principles of Functional Programming: substitution model, for-expressions and how they relate to monads. Introduces a new implementation of for-expressions: random value generators. Shows how this can be used in randomized testing and gives an overview of ScalaCheck, a tool which implements this idea.
• Week 2: Functional programming and mutable state. What makes an object mutable? How this impacts the substitution model. Extended example: Digital circuit simulation.
• Week 3: Futures. Introduces futures as another monad, with for-expressions as concrete syntax. Shows how futures can be composed to avoid thread blocking. Discusses cross-thread error handling.
• Week 4: Reactive stream processing. Generalizing futures to reactive computations over streams. Stream operators.
• Week 5: Actors. Introduces the Actor Model, actors as encapsulated units of consistency, asynchronous message passing, discusses different message delivery semantics (at most once, at least once, exactly once) and eventual consistency.
• Week 6: Supervision. Introduces reification of failure, hierarchical failure handling, the Error Kernel pattern, lifecycle monitoring, discusses transient and persistent state.
• Week 7: Conversation Patterns. Discusses the management of conversational state between actors and patterns for flow control, routing of messages to pools of actors for resilience or load balancing, acknowledgement of reception to achieve reliable delivery.

Recommended Background:

You should have a background equivalent to someone who completed the course “Principles of Functional Programming”. We assume you know the fundamentals of functional programming and the Scala language.

А почему бы не разрешить корректорам вносить изменения в опросы?

Сейчас корректорам приходится совершать слишком много действий:

• прилетело уведомление;
• тыкаем «править» и видим, что редактировать можно только заголовок и теги;
• идем в корректорскую рассылку или пишем модератору в джаббер;
• ?????
• PROFIT!

Дискасс.

16 июля 2013 года проекту DragonFly BSD исполнилось 10 лет. Эта операционная система возникла из четвертой ветки FreeBSD из-за разногласий между разработчиками. Мэтт Диллон был недоволен работой по оптимизации ядра FreeBSD, поэтому принял решение о создании новой операционной системы, предназначенный для работы на высоконагруженных серверах и многопроцессорных системах.

За 10 лет работы команде разработчиков удалось построить операционную систему, ушедшую довольно далеко от оригинальной FreeBSD:

• в ядре используется легковесные потоки (LWKT);
• существенным образом переработан планировщик, который показывает неплохие результаты в синтетических тестах;
• для замены UFS разработана версионная файловая система HAMMER.

>>> Подробности

Опубликован очередной квартальный отчет, который охватывает проекты, развиваемые под эгидой FreeBSD.

Период с апреля по май выдался достаточно интересным для приверженцев этой открытой операционной системы:

• проведены BSDCan и FreeBSD Developer Summit;
• улучшена поддержка AMD GPU;
• добавлены новые драйверы для сетевого оборудования;
• поддержка ZFS TRIM;
• улучшена поддержка Xen.

>>> Подробности

OCaml-Top — интерактивный редактор, разработанный для новичков, изучающих язык программирования OCaml.

Этот редактор не претендует на место tuareg-mode и других плагинов, добавляющих поддержку OCaml в популярные IDE, поэтому довольно ограничен в возможностях:

• подсветка синтаксиса;
• автоматическое форматирование кода;
• интуитивно понятные элементы запуска и пошагового выполнения;
• подсветка ошибок.

На GNU/Linux и OSX OCaml-Top доступен из opam. Для операционных систем семейства Windows подготовлены бинарные пакеты.

Исходные коды OCaml-Top распространяются на условиях лицензии GPLv3.

>>> Подробности

В этом году приз Programming Languages Software Award достался Coq.

!Ъ: тыц

Ъ:

The Coq proof assistant provides a rich environment for interactive development of machine-checked formal reasoning. Coq is having a profound impact on research on programming languages and systems, making it possible to extend foundational approaches to unprecedented levels of scale and confidence, and transfer them to realistic programming languages and tools. It has been widely adopted as a research tool by the programming language research community, as evidenced by the many papers at SIGPLAN conferences whose results have been developed and/or verified in Coq. It has also rapidly become one of the leading tools of choice for teaching the foundations of programming languages, with courses offered by many leading universities and a growing number of books emerging to support them. Last but not least, these successes have helped to spark a wave of widespread interest in dependent type theory, the richly expressive core logic on which Coq is based.

As a software system, Coq has been in continuous development for over 20 years, a truly impressive feat of sustained, research-driven engineering. The Coq team continues to develop the system, bringing significant improvements in expressiveness and usability with each new release.

In short, Coq is playing an essential role in our transition to a new era of formal assurance in mathematics, semantics, and program verification.

CompCert — это компилятор языка программирования Си (ANSI C с незначительными ограничениями) для платформ PowerPC, ARM и IA32, предназначенный для сборки программ с повышенными требованиями надежности и дополняющий формальные методы проверки (статический анализ, проверка на модели и т.п.) на уровне исходного кода.

Некоторые изменения:

• поддержка типов long long и unsigned long long;
• предварительная поддержка отладочной информации;
• агрессивная стратегия исключения дублирующегося кода;
• уменьшено потребление памяти при компиляции;
• исправлены некоторые ошибки.

Исходные коды компилятора распространяются на условиях лицензии «INRIA Non-Commercial License Agreement».

>>> Подробности

Некто Andrej Bauer закончил работу над сабжевой книгой.

http://homotopytypetheory.org/book/

Исходники книги распространяются на условиях лицензии Creative Commons Attribution-ShareAlike 3.0 Unported License.

Скачать сорцы без регистрации и смс можно тут.

Вышла публичная бета книжки Real World OCaml.

Книга содержит три большие раздела: «Language Concepts» (общее описание языка), «Tools and Techniques» (hashtables, работа с json и т.п.) и «The Runtime System» (FFI, GC).

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

Более подробно: есть сервис, который предоставляет пользователям всякие разные плюшки, планируется добавить видеонаблюдение. Продажники хотят продавать не объем дискового пространства, доступный за определенную абонентскую плату, а глубину архива — три дня/неделя и т.п. В процессе тестирования мы соберем некоторую статистику по необходимому размеру дискового пространства. Стоит задача организовать некий циклический архив для пользователя.

Каким образом это проще всего сделать?

Состоялся релиз Linux Mint 15 — наиболее значимый выпуск с момента старта проекта, по мнению разработчиков. Значительно улучшен MATE 1.6, Cinnamon 1.8 содержит множество изменений, таких как хранитель экрана и единый центр управления.

Некоторые изменения:

• MDM содержит три новых компонента:
  • GTK greeter;
  • GTK greeter с поддержкой множества тем оформления;
  • HTML greeter поддерживает анимированные темы оформления, созданные с использованием HTML5, CSS, Javascript, WebGL.
• В новый выпуск включено приложение Software Sources (MintSources) для управления источниками приложений.
• Новое приложение MintDrivers призвано упростить установку драйверов оборудования, включая проприетарные и альтернативные драйверы.

Подробный иллюстрированный обзор новшеств и изменений доступен на официальном сайте проекта.

«Рандомизация и бутстрап: статистический анализ в биологии и экологии с использованием R» — альманах статистических методов, иллюстрированный примерами биологического характера.

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

Электронная версия книги «как она есть» пока распространяется без всяких ограничений (до возможного появления договорных обязательств).

Скрипты на R по всем обсуждаемым примерам приведены в конце каждого раздела. Исходные данные для анализа и коды R доступны в электронном виде.

>>> Подробности

N2O (Nitrogen 2x Optimized) — это усовершенствованная версия знаменитого Erlang веб фреймворка Nitrogen, но работающая полностью на вебсокетах и в несколько раз быстрее оригинального Нитрогена.

Основные изменения:

• оптимизация всех слоев;
• использование бинарного протокола BERT для контролов;
• отложенная доставка JavaScript на клиент;
• совместим по стилям с Twitter Bootstrap;
• минимальное количество Erlang процессов на запрос;
• поддержка шаблонов DTL;
• быстрая разработка REST приложений;
• XHR Fallback для старых браузеров без поддержки WebSockets;
• размер исходников сокращен до 3000 строк;
• поддержка Zepto для не IE браузеров.

Страница проекта на GitHub.
Домашняя страница.
Презентация.

Собственно, сабж.

Книга «Рандомизация и бутстреп: статистический анализ в биологии и экологии с использованием R»:

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

Скачать бесплатно без смс