Статья 340

Это наблюдение о типах в значительной мере переносится и на более сложные и выразительные языки и легло в основу целой теории в приложениях конструктивной математики исчисления формул как типов П. Мартин-Лефа.
Наблюдение же об изоморфности вывода и извлекаемой из него программы, подобно более примитивному случаю Пролога, сыграло дезориентирующую роль, но на следующем уровне, на самом деле поддержать такой изоморфизм для достаточно выразительных языков почти невозможно.

Логика схем программ.

Логика схем программ, изобретенная в 80-х годах, использует наблюдения, сделанные нами при анализе простейшей импликативной логики
Мы видели, что одним из труднейших мест в логическом описании программ является цикл. Основная сложность в том, что каждый шаг цикла должен приближать нас к его завершению, а это не просто описать в обычной логике, где, как известно, невыразимо даже понятие конечного множества.