Union of Reducibility Candidates for Orthogonal Constructor Rewriting

We revisit Girard's reducibility candidates by proposing a general of the notion of neutral terms. They are the terms which do not interact with some contexts called elimination contexts. We apply this framework to constructor rewriting, and show that for orthogonal constructor rewriting, Girard's reducibility candidates are stable by union.

• Type: Conference
• Year: 2008
• Where: CIE
• Authors: Colin Riba
• Keywords: Applied Computing, CIE 2008, Contexts Called Elimination, Girard's Reducibility Candidates, Neutral Terms