On completeness of reducibility candidates as a semantics of strong normalization

DOI10.2168/LMCS-8(1:3)2012zbMath1239.03033arXiv1201.1705OpenAlexW2073404010MaRDI QIDQ2881069

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)

Uses Software

• Coq
• dedukti

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