Why the Usual Candidates of Reducibility Do Not Work for the Symmetric λμ-calculus
作者： René David , Karim Nour
DOI: 10.1016/J.ENTCS.2005.06.020
关键词:
摘要: The symmetric @[email protected] is the introduced by Parigot in which reduction rule @m^', of @m, added. We give examples explaining why technique using usual candidates reducibility does not work. also prove a standardization theorem for this calculus.
core.ac.uk
elsevier.com
univ-savoie.fr 
sci-hub.se 参考文章(24)
Robert Constable, Chet Murthy, Finding computational content in classical proofs Logical Frameworks. pp. 341- 362 ,(1991) , 10.1017/CBO9780511569807.014
Niels Jakob Rehof, Morten Heine Sørensen, The λΔ-calculus international symposium on theoretical aspects of computer software. pp. 516- 542 ,(1994) , 10.1007/3-540-57887-0_113
Michel Parigot, Classical Proofs as Programs KGC '93 Proceedings of the Third Kurt Gödel Colloquium on Computational Logic and Proof Theory. pp. 263- 276 ,(1993) , 10.1007/BFB0022575
René David, Karim Nour, Arithmetical Proofs of Strong Normalization Results for Symmetric λ-calculi international conference on typed lambda calculi and applications. ,vol. 77, pp. 489- 510 ,(2007) , 10.1007/11417170_13
Morten Heine Sørensen, Jakob Rehof, The LambdaDelta-calculus international conference on theoretical aspects of computer software. pp. 516- 542 ,(1994)
Karim Nour, Non Deterministic Classical Logic: The lambda-mu ++ -calculus. Mathematical Logic Quarterly. ,vol. 48, pp. 357- 366 ,(2002) , 10.1002/1521-3870(200204)48:3<357::AID-MALQ357>3.0.CO;2-L
Yoriyuki Yamagata, Strong Normalization of Second Order Symmetric Lambda-mu Calculus international symposium on theoretical aspects of computer software. pp. 459- 467 ,(2001) , 10.1007/3-540-45500-0_23
Philippe de Groote, A Simple Calculus of Exception Handling international conference on typed lambda calculi and applications. pp. 201- 215 ,(1995) , 10.1007/BFB0014054
Jean-Yves Girard, A new constructive logic: classic logic Mathematical Structures in Computer Science. ,vol. 1, pp. 255- 296 ,(1991) , 10.1017/S0960129500001328
Karim Nour, Khelifa Saber, A semantical proof of the strong normalization theorem for full propositional classical natural deduction Archive for Mathematical Logic. ,vol. 45, pp. 357- 364 ,(2006) , 10.1007/S00153-005-0314-Y