?

Log in

No account? Create an account
Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Формализация криптографических протоколов. [May. 23rd, 2018|01:51 pm]
Программирование с зависимыми типами

potan
[Tags|]

Кто-нибудь занимается описанием криптографических протоколов с помощью зависимых типов? Это было бы полезно, например, для верификации смартконтарктов.
Там возникают сложности, как описать знание/незнание ключа. Похоже, полноценного описания требуется использовать модальную логику - такие логики могут отображаться в системы типов?
Пока получается что-то вроде:

Хеш-функция

hash: Data -> CheckSum
hashProp1: (x:Data) -> (y:Data) -> (hash x = hash y) -> (x = y)
hashProp2: (rev: CheckSum -> Data) -> (p: (d: Data -> rev (hash d) = d)) -> Void

То есть значение хеш-функции однозначно идентифицирует аргемент, но обратной к ней не существует.

Симметричное шифрование

encode: Key -> Data -> Encrypted
decode: Key -> Encrypted -> Data
cryptProp1: (k: Key) -> (d: Encrypted) -> (encode k (decode k d)) = d
cryptProp2: (k: Key) -> (d: Data) -> (decode k (encode k d)) = d
cryptProt3: ((d:Data, e:Encrypt) -> (k: Key ** (encode k d = e))) -> Void
cryptProp4: (((d1:Data, e1:Encrypt) -> (d2:Data, e2:Encrypt) -> Either (k: Key -> encode k d1 = e1 -> encode k d2 = e2) (k: Key -> encode k d1 = e1 -> encode k d2 = e2 -> Void)

С электронной подписью пока не разобрался.
Link1 comment|Leave a comment

Зависимые типы и high kind types. [Oct. 27th, 2017|11:55 am]
Программирование с зависимыми типами

potan
[Tags|]

Есть вполне полезные языки, не поддерживаюшие HKT - Rust, Elm. Возможно ли (и осмысленно) в подобных языках делать поддержку зависимых типов? Например, Elm справедливо требует тотальности кода, но из-за этого приходится описывать и обрабатывать невозможные ситуации, например когда пользователь еще не залогинился, а уже разлогинивается. Зависимые типы позволяют описать невозможность такого события.
Link4 comments|Leave a comment

Как матчит Агда? [Oct. 16th, 2013|08:59 pm]
Программирование с зависимыми типами
nealar
[Tags|]

В брутальном [мета-]введении в Агду попался пример

data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {n m} → n ≤ m → succ n ≤ succ m

sub₀ : (n m : ℕ) → m ≤ n → ℕ
sub₀ n zero (z≤n .{n}) = n
sub₀ .(succ n) .(succ m) (s≤s {m} {n} y) = sub₀ n m y

Не могу понять, как определение sub0 раскрывается в case, а главное, почему так.

Тайна раскрыта
Агда матчит в том порядке, в котором написано в программе: по первой строчке выбирается паттерн с конструктором, соответствующая переменная раскрывается в case, и так далее.
Ошибка oxij в том, что по аргументам с точкой паттерн-матчить вообще нельзя

Приз "за лучшую подсказку" уходит к nivanych
Link16 comments|Leave a comment

Dependently-Typed Metaprogramming in Agda by Conor McBride [Aug. 30th, 2013|12:26 am]
Программирование с зависимыми типами

lelf
https://www.youtube.com/channel/UCqm9psjm_czCS0EXCjr3A4w
LinkLeave a comment

The HoTT Book [Jun. 21st, 2013|02:53 pm]
Программирование с зависимыми типами

nivanych
http://homotopytypetheory.org/book/
http://homotopytypetheory.org/2013/06/20/the-hott-book/
http://golem.ph.utexas.edu/category/2013/06/the_hott_book.html
LinkLeave a comment

Уникальные типы в Агда [Jan. 24th, 2013|12:30 am]
Программирование с зависимыми типами
dima_starosud
[Tags|]

Теперь можно доказывать корректность императивных программ с помощью зависимых типов.
Link1 comment|Leave a comment

Введения в Agda [Jan. 23rd, 2013|11:09 pm]
Программирование с зависимыми типами

deni_ok
[Tags|]

Пара хороших введений в Агду. Оставлю здесь, чтобы было куда ссылаться.

Peter Divianszky (Eötvös Loránd University, Department of General Computer Science)
https://people.inf.elte.hu/divip/AgdaTutorial/Index.html

Thorsten Altenkirch (School of Computer Science, the University of Nottingham)
http://www.cs.nott.ac.uk/~txa/g53cfr/
Link7 comments|Leave a comment

coq затык [Nov. 17th, 2010|09:51 pm]
Программирование с зависимыми типами

zelych
Подскажите, пожалуйста.
Вот у меня есть индуктивный предикат:
  Inductive last (a: A): list A -> Prop :=
  | last_one: last a (a :: nil)
  | last_many: forall (l: list A) (x: A), last a l -> last a (x :: l).

Очевидно?, что last a nil быть не может. Как тогда доказать что-нибудь типа такого?
  Lemma last_nil: forall (a: A), last a nil -> False.

Спасибо.
Link5 comments|Leave a comment

кортежи с именованными компонентами как dependent product [Jul. 20th, 2010|04:11 am]
Программирование с зависимыми типами

beroal
Рассмотрим типизированные кортежи с именованными компонентами. Множество имён компонентов KS одно для всех кортежей, но кортеж может иметь не все компоненты. Есть функция typeof, которая отображает имя компонента на тип компонента. Множество функций с зависимым типом, у которых зависимость типа результата от значения аргумента задаётся typeof, и есть множество кортежей с компонентами из KS.

KS0 ⊆ KS ∧ KS1 ⊆ KS. Если истинно KS0 ⊆ KS1, то существует проекция, которая берёт кортеж с именами KS1 и возвращает кортеж с именами KS0. Проекция всего лишь выбрасывает те компоненты кортежа, имена которых ∈ KS1 и ∉ KS0, потому я назвал её проекцией. KS0 ⊆ KS1 можно превратить как каноническую инъекцию inj : KS0 → KS1. Тогда интуитивно это описывается как «инъекция превращается в проекцию». Если построить категорию (обозначим её (P KS)) из ЧУМ подмножеств KS, имею контравариантный функтор D : P KS → Set (и пучок).

Как доказать свойства D из свойств dependent product? typeof использовать не получится, вместо typeof имеем bundle для каждого KS0, KS0 ⊆ KS. pullback functor inj* должен отображать bundle для KS1 в bundle для KS0, bundle-ы разумеется связаны. Морфизм KS0→1 (назову его (final KS0)) (1 — это singleton, я работаю в Set) задаёт функтор Π (final KS0), который берёт bundle для KS0 и возвращает собственно множество кортежей с именами KS0.

Дальше затык. Информация по dependent product у меня очень скудная.
Link2 comments|Leave a comment

сайт вопросов и ответов, посвящённый информатике [Jul. 16th, 2010|02:39 am]
Программирование с зависимыми типами

beroal
то бишь computer science. Здесь собирают подписи.
LinkLeave a comment

navigation
[ viewing | most recent entries ]
[ go | earlier ]