Previous Entry Share Next Entry
photo25

(repost) Вакансия Ассистента Рисерчера

Оригинал взят у maxim в Вакансия Ассистента Рисерчера
Друзья! У нас появилось немного денег, которые мы хотим потратить. В нашу эрланг компанию требуется стажер, возможно студент, который интересуется теорией типов и разработкой компиляторов. Если так получилось что вы родились в Украине, и вам тесно и грустно работать перекладывая байты из JSON в XML на Хаскеле, но вас не берут в крутые международные проекты под управлением Аводея, Байера и Мейера из-за отсутствия публикации -- это все поправимо.

Что мы предлагаем? Мы предлагаем вам присоединится к нам в качестве ассистента или младшего научного сотрудника. Все публикации, авторские права остаются за вами, никакого NDA или прочей непределенности. Все статьи публикуются на превью прощадки как только достигнут качества "не стыдно".

Мы исследуем разные аспекты компиляции эрланг кода и компиляции в контексте эрланг инфраструктуры, так, например, компания Cloudozer занимается разрабткой статически-компилируемого LLVM языка L, основное назначение которого генерировать эффективный нативный код (с удалением информации о типах) из исходников похожих на Эрланг или с минимальными изменениями Эрланг кода. Synrc же занимается фул стек Erlang решениеми и исследованием в области доказательства корректности программ. Сейчас у нас есть два направления: 1) это доказательство алгоритмов используемых для обеспечения персистентного хранения цепочек (KVS/N2O/BPE), используя пруверы основанные на теории зависимых типов (мы используем Lean, вы должны уметь использовать любой прувер с Pi типами); 2) разработка собственного языка с рекурсивными полиномиальными типами и зависимыми рекордами (первоклассными модулями), который компилируется в промежуточную форму чистого языка на основе Henk/Morte/Om, а оттуда транформируется в Erlang AST (без компиляции паттерн мачинга, без необходимости своего gc, т.е. все самое сложное оставляем для виртуальной машины Эрланг и его оптимизирующего компилятора).

Что мы хотим? Мы хотим, чтобы вы знали основы Теории Категорий, могли нарисовать все коммутативные диаграммы и аксиомы необходимые для определния декартово-замкнутой категории и могли читать proof-theoretical аксиоматическую нотацию. Также вы должны понимать коммутативные диаграммы F-алгебр для рекурсивных типов, а также иметь понятие о кодировании Черча и его применении к кодированию индуктивных типов. Необязательно но полезно было бы быть знакомым со слоениями и slice категориями для категорного понимания зависимых типов.

Поверьте, такой опыт предложить в Украине не может ни одна компания. Важно иметь возможность проводить еженедельные совещания в оффлайне, удаленная работа полностью исключается.

Пишите: maxim@synrc.com


  • 1
maxim January 5th, 2016
Данке Шон!

amarao_san January 5th, 2016
Звучит красиво, да. Теория Категорий в контексте зависимых типов и доказательства правильности - это когда есть очень категоричный, но зависимый тип, и он всем доказывает, что он прав.

wizzard0 January 5th, 2016
лучший!

  • 1
?

Log in

No account? Create an account