That specific formalism is only specific to McCarthy's implementation though,

Not even that. It's the programmatic definition of the core of Lisp. McCarthy's real Lisp implementation was much more featureful.

I would also think the Lisp program in the second paper is 'Lisp Program Zero'. ;-) If your language can run it, it is Lisp. The amount of modifications necessary (syntactic, operators, semantics, ...) gives an indication how far another language is away from it.

Here is a version in Common Lisp:

https://gist.github.com/lispm/d752d5761f7078de4041d4e453e70c...