Note that this actually works in ancient, dynamically scoped dialects of Lisp, and will work with dynamically scoped variables.

  (progv '(a) '(10) (eval '(+ a 1)))  ;; Common Lisp, TXR Lisp

With lexical scope, what you're looking for is a closure. lambda is your "first class quote".

  [1]> (defmacro fcquote (expr) `(lambda () ,expr))
  FCQUOTE
  [2]> (defun fceval (fcq) (funcall fcq))
  FCEVAL
  [3]> (fceval (let ((a 10)) (fcquote (+ a 10))))
  20

> Hygienic macros are just a band aid ...

Sure, whatever; what I intended to bring up was the specific way of implementing hygienic macros using syntactic closures. Syntactic closures are a way of quoting code, with context. Hygienic macros don't have to be implemented with syntactic closures.

That author you cited seems to be working on something very similar to syntactic closure. The paper has a lot of references, but very few of them are anything Lisp or Scheme related. Looks like the author is working entirely on his own.

In a work like this, I'd expect syntactic closures to be acknowledged, with a discussion of how the work being presented is different.

Syntactic closures are a way to hide the fact that lambdas are the only abstraction in lambda calculus.

The work that I cited has types _and_ quotation as first class abstractions.

It's a bit like asking to explain proof theory in terms of Godel numbers. Sure you can technically do it. You're completely missing the point if you do however.

I think syntactic closures don't have to be concerned with type, because their job is just to ensure that the symbols included in a quote refer to what they are supposed to refer to, regardless to where that quote is moved. When the closures are evoked, reasoning about types can take place then.