On completeness of reducibility candidates as a semantics of strong normalization

This paper defines a sound and complete semantic criterion, based onreducibility candidates, for strong normalization of theories expressed inminimal deduction modulo \`a la Curry. The use of Curry-style proof-termsallows to build this criterion on the classic notion of pre-Heyting algebrasand makes that criterion concern all theories expressed in minimal deductionmodulo. Compared to using Church-style proof-terms, this method provides both asimpler definition of the criterion and a simpler proof of its completeness.Comment: 24 page