Title: The strength of the subset type in Martin-Lof's type theory
Abstract: The authors show that the exact formulation of the rules of type theory is important for rules of subset type. It turns out that there are propositions involving subsets that are trivially true in naive set theory, but which cannot be proved in type theory. They examine the probability of a type proposition that is important when modularizing program derivations.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
Publication Year: 2003
Publication Date: 2003-01-06
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 20
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot