Denis Cousineau - On completeness of reducibility candidates as a semantics of strong normalization

lmcs:845 - Logical Methods in Computer Science, February 16, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:3)2012
On completeness of reducibility candidates as a semantics of strong normalization

Authors: Denis Cousineau

    This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo à 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.


    Volume: Volume 8, Issue 1
    Published on: February 16, 2012
    Accepted on: June 25, 2015
    Submitted on: May 16, 2011
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    Share

    Consultation statistics

    This page has been seen 323 times.
    This article's PDF has been downloaded 309 times.