Первый Теоретикотиповой
Категорный Митап в Киеве!



Митап будет проходить весной-летом в HUB4.0, следите за новостями. На митапе будет представлено три доклада:

1. Введение в зависимые типы (Кириллов)
2. Кодировки пространства (Лютко)
3. Презентация теорем прувера (Сохацкий)


В мире типизированного лямбда-исчисления есть более слабая и надежная формальная система Calculus of Construction (CoC), единственной операцией на типах в которой является тип зависимых функций, а также более сильная и выразительная Calculus of Inductive Constructions (CIC), включающая индуктивные типы. Предположим, мы хотим использовать в нашем языке все преимущества наличия индуктивных типов CIC, оставив бекэнд простым, основанным на CoC. Классические методы достигнуть этого — так называемые кодировки, например, кодировка Черча-Бёма-Берардуччи, — либо не позволяют выразить в получившейся системе аксиому индукции, необходимую для полноценного обращения с зависимыми типами, либо требуют расширения CoC другими экзотическими операциями. Сегодня мы опишем кодировку индуктивных и коиндуктивных типов, работающую в неизмененном CoC, которая основана на использовании известных конструкций из теории категорий. Будут рассмотрены варианты кодировки для непредикативной и предикативной иерархии универсумов, а также для кодирования самого типа-универсума. Кодировка допускает обобщение на высшие индуктивные типы в таких современных вариантах теории типов, как HoTT.

Target audience: type theoretical enthusiasts, mathematicians, computer scientists, functional programmers

Список рекомендованной литературы:

1. Benjamin C. Pierce, Basic category theory for computer scientists, MIT Press, 1991

2. Peng Fu, Lambda encodings in type theory, University of Iowa, 2014

Индуцируй с нами, индуцируй как мы, индуцируй лучше нас!

Контакты организаторов: +380676631870 Максим [email protected]





Events | Privacy Policy | Feedback | Brandbook
Copyright © 2005–2016 Synrc Research Center s.r.o.