A Type-Theoretic Framework for Formal Reasoning with Different Logical Foundations

Abstract. A type-theoretic framework for formal reasoning with different logical foundations is introduced and studied. With logic-enriched type theories formulated in a logical framework, it allows various logical systems such as classical logic as well as intuitionistic logic to be used effectively alongside inductive data types and type universes. This provides an adequate basis for wider applications of type theory based theorem proving technology. Two notions of set are introduced in the framework and used in two case studies of classical reasoning: a predicative one in the formalisation of Weyl's predicative mathematics and an impredicative one in the verification of security protocols.

• Type: Conference
• Year: 2006
• Where: ASIAN
• Authors: Zhaohui Luo
• Keywords: Algorithms, ASIAN 2006, Logic-enriched Type Theories, Logical Framework, Various Logical Systems