Beniamino Accattoli (2013):
Linear Logic and Strong Normalization.
In: Femke van Raamsdonk: 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
LIPIcs 21.
Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik,
Dagstuhl, Germany,
pp. 39–54,
doi:10.4230/LIPIcs.RTA.2013.39.
Beniamino Accattoli & Delia Kesner (2010):
The Structural λ-Calculus.
In: Anuj Dawar & Helmut Veith: Computer Science Logic,
LNCS 6247.
Springer Berlin Heidelberg,
pp. 381–395,
doi:10.1007/978-3-642-15205-4_30.
Vincent Danos & Laurent Regnier (2004):
Head Linear Reduction.
Http://iml.univ-mrs.fr/~regnier/articles/pam.ps.gz.
R. O. Gandy (1980):
Proofs of strong normalisation.
In: J. P. Seldin & J. R. Hindley: To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism.
Academic Press,
pp. 457–477.
Stefano Guerrini & Giulio Pellitta (2016):
Dissecting the PAM.
Submitted.
Alexandre Miquel:
A combinatorial proof of strong normalisation for the simply typed -calculus.
Unpublished draft.
Pierre-Marie Pédrot & Alexis Saurin (2016):
Classical By-Need.
In: Peter Thiemann: Programming Languages and Systems. 25th European Symposium on Programming, ESOP 2016,
LNCS 9632.
Springer,
pp. 616–643,
doi:10.1007/978-3-662-49498-1_24.
Laurent Regnier (1994):
Une équivalence sur les lambda-termes.
Theoretical Computer Science 126(2),
pp. 281–292,
doi:10.1016/0304-3975(94)90012-4.