On completeness of reducibility candidates as a semantics of strong normalization

DOI10.2168/LMCS-8(1:3)2012MaRDI QIDQ2881069zbMATH OpenOpenAlexFDO

Authors Denis Cousineau

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1201.1705

zbMATH Keywords

completeness theoremstrong normalizationreducibility candidatesChurch proof-termsCurry proof-termsminimal deduction modulo

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

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.

Recommendations

• A Semantic Proof that Reducibility Candidates entail Cut Elimination
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• New Computational Paradigms
• Continuous semantics for strong normalisation
• scientific article; zbMATH DE number 512779

Cited in

(2)

• Union of Reducibility Candidates for Orthogonal Constructor Rewriting
• Programming Languages and Systems

Describes a project that uses

Uses Software

• dedukti
• Coq

This page was built for publication: On completeness of reducibility candidates as a semantics of strong normalization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881069)