Я читал эту статью http://www21.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf.
На странице 7 она содержит исчисление для системы типов Изабель. В этом исчислении «термин имеет тип» и «доказательство имеет термин».
1) Существует ли более подробная статья по этому исчислению?
2) Единственные два правила, которые я не понимаю, - это те, которые относятся к константам.
2.1) Что означает "c _ {[\ vec {\ tau} _n / \ vec {\ alpha} _n]}"? Это доказательства, которые являются константами.У нас есть, например, константа «impI» на странице 9. Как эти тау и альфа связаны с «термином impI».
2.2) Не могли бы вы уточнить правило $ \ Sigma (c)[\ vec {\ tau} _n / \ vec {\ alpha} _n] $. ?
На первый взгляд это можно перевести как «любой набор терминов, которые зависят от константы доказательства (!) с любым количествомтипов вместо атомарных типов ", но я не вижу в этом никакого смысла.
3) Я также заинтересован в работах по семантике этого исчисления и / или теореме о корректности его .
Я ценю любую связанную информацию.Спасибо!