Карри-Говард для синтеза терминов в Изабель

Question

Скажем, я доказал некоторые основные положения интуиционистской логики высказываний в Изабель /HOL:

theorem ‹(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))›
proof -
  {
    assume ‹A ⟶ B›
    {
      assume ‹B ⟶ C›
      {
        assume ‹A›
        with ‹A ⟶ B› have ‹B› by (rule mp)
        with ‹B ⟶ C› have ‹C› by (rule mp)
      }
      hence ‹A ⟶ C› by (rule impI)
    }
    hence ‹(B ⟶ C) ⟶ (A ⟶ C)› by (rule impI)
  }
  thus ?thesis by (rule impI)
qed

Я знаю из соответствия Карри-Говарда, что предложение соответствует некоторому типу (a -> b) -> ((b -> c) -> (a -> c))и доказательство некоторому члену, все внутри некоторой теории типов (скажем, в λ-исчислении с простым типом). Из структуры доказательства я знаю, что соответствующий типизированный λ-член λf:a→b. λg:b→c. λx:a. f(g(x)),

Есть ли способ заставить Изабель построить это для меня?

Я посмотрел на извлечение программ в Изабелле, и из того, что я могу сказать, это в значительной степени относится к чему-то другому: где вы пишете функциональные программы на Изабель, доказываете что-то о них, а затем это обеспечивает своего рода перевод на Хаскель или ML.

Я также знаю, что HOL - это не то же самое, что теория зависимых типов, которая, как я понимаю, имеет более сильный вкус Карри-Ховарда. Я знаю, что сам HOL концептуально в некотором роде похож на полиморфное λ-исчисление, и я нашел несколько кратких заметок о том, как HOL является поверхностным кодированием логики в теории типов, но будет весьма полезен некоторый дополнительный контекст. Я едва смог собрать воедино, как все эти разные помощники по доказательству и связанные с ними основы связаны друг с другом, и, возможно, какой-то более исторический контекст тоже поможет. К сожалению, документация вокруг Изабель, Кок и т. Д. Кажется немного повсеместной; в частности, для Изабель, я, кажется, регулярно нахожу информацию, которая устарела на 20 лет.