On completeness of reducibility candidates as a semantics of strong normalization
Logic in Computer Science
2015-07-01 v2
Abstract
This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo \`a la Curry. The use of Curry-style proof-terms allows to build this criterion on the classic notion of pre-Heyting algebras and makes that criterion concern all theories expressed in minimal deduction modulo. Compared to using Church-style proof-terms, this method provides both a simpler definition of the criterion and a simpler proof of its completeness.
Keywords
Cite
@article{arxiv.1201.1705,
title = {On completeness of reducibility candidates as a semantics of strong normalization},
author = {Denis Cousineau},
journal= {arXiv preprint arXiv:1201.1705},
year = {2015}
}
Comments
24 pages