Union of Reducibility Candidates for Orthogonal Constructor Rewriting

Colin Riba (1)

1 EVEREST - Environments for Verification and Security of Software

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.

Mots clés: lambda-calculus; rewrite systems; strong normalization; reducibility; union types

Domaines: Logique en informatique [cs.LO]

Colin Riba. Union of Reducibility Candidates for Orthogonal Constructor Rewriting. 2008. ⟨inria-00204710⟩