deniok: (lambda cube)
Очень хорошие лекционные заметки Femke van Raamsdonk'а из Vrije Universiteit Amsterdam. Курс похож на тот, что я читал в CS Club'е при ПОМИ, но с несколько большим уклоном в логику и примерами с использованием Coq.
Рекомендую своим студентам как полезное дополнительное чтение и удобное введение в Coq.
deniok: (lambda cube)
Сегодняшние вести с LtU: Certified Programming With Dependent Types
Книжка про COQ, судя по оглавлению весьма полезная. Не пропустите, кто интересуется заявленными темами.
deniok: (lambda cube)
Simon Peyton Jones, Chung-Chieh Shan и Oleg Kiselyov обещают статью "Fun with type functions", а пока выложили слайды. После впечатляющих примеров на Хаскелле с использованием индексированных семейств типов и функций над типами, радует замечание на последнем слайде:
At some point it may be best to say “enough fooling around: just use Coq”. But we aren’t there yet.
Хорошее, годное замечание.
deniok: (typed lambda)
У него там неонка дджин внутри. Тактика tauto доказывает пропозициональные тавтологии, монтируя лямбда-терм подходящего типа

Coq < Variables A B C : Prop.
A is assumed
B is assumed
C is assumed

Coq < Lemma he_he : (B -> C) -> (A -> B) -> A -> C.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (B -> C) -> (A -> B) -> A -> C

he_he < tauto.
Proof completed.

he_he < Qed.
 tauto.
he_he is defined

Coq < Print he_he.
he_he =
fun (H : B -> C) (H0 : A -> B) (H1 : A) =>
let H2 := H0 H1 in let H3 := H H2 in H3
     : (B -> C) -> (A -> B) -> A -> C
Здесь fun вместо лямбды и типизация связанных в лямбда-терме переменных явная, чёрчевская.

Но можно и примитивными тактиками intros; apply H; apply H0; assumption:Read more... )Всякому видно, что при ручной работе и терм-композитор выходит кратким и выразительным, не то что эти вложенные let'ы ;-)
deniok: (Default)
Скачал и поставил COQ. Это, если кто не знает, СУФД - система управления формальными доказательствами :-) Так у них на сайте написано
Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine.




Читаю крэш-курс Coq in a Hurry.

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 25th, 2017 02:53 pm
Powered by Dreamwidth Studios