Очень хорошие лекционные заметки Femke van Raamsdonk'а из Vrije Universiteit Amsterdam. Курс похож на тот, что я читал в CS Club'е при ПОМИ, но с несколько большим уклоном в логику и примерами с использованием Coq.
Рекомендую своим студентам как полезное дополнительное чтение и удобное введение в Coq.

Simon Peyton Jones, Chung-Chieh Shan и Oleg Kiselyov обещают статью "Fun with type functions", а пока выложили слайды. После впечатляющих примеров на Хаскелле с использованием индексированных семейств типов и функций над типами, радует замечание на последнем слайде: Хорошее, годное замечание.

У него там неонка дджин внутри. Тактика 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'ы ;-)