Есть два подхода к вкладыванию логики в системы типов. Прямое представление (благодаря Карри-Говарду): одна система типов - одна логика. И Logical Framework, когда в одну систему типов можно вложить несколько разных логик, при этом правила конкретной логики объявляются в контексте.

"Система записи" - это и то и другое.