From: bcpierce@cis.upenn.edu
Subject: JFP-2013-0041 - Decision on Manuscript
Date: 9 June 2014 3:57:39 AEST
To: benl@ouroborus.net
Cc: MatthiasFelleisen , JeremyGibbons , jfp-ed@cambridge.org, bcpierce@cis.upenn.edu
Dear Ben:
Your manuscript ID JFP-2013-0041 entitled "Mechanized soundness for a type and effect system with region deallocation," which you submitted to the Journal of Functional Programming, has been reviewed. The comments of the referees are included at the bottom of this letter.
As you'll see, the top-level recommendations of the reviewers range from "accept" to "reject and resubmit" -- seemingly a very wide range, until you look at the actual comments, which are fairly consistent: They reviewers seem to basically like what is there (modulo a number of suggestions for simplification, polishing, and minor generalization), but feel that (a) the technical contribution is perhaps a little thin, in the sense that paper proofs of similar properties for similar systems are well known and the formalization itself does not seem to involve significant new techniques, and (b) the motivation for studying this particular system (as opposed to a more modern and flexible one) is not completely convincing.
I think the best way to proceed is for you to take a look at the reviews, paying particular attention to these points, and form your own opinion as to the best way to address the reviewers' concerns -- in particular, how to increase the technical novelty and pragmatic motivation for the system you're formalizing with reasonable effort. Before actually undertaking the revisions, though, please drop me an email describing your plans so that I and the reviewers can give you an early reading on whether the changes you have in mind will be satisfactory.
When the time comes to revise your manuscript, log into http://mc.manuscriptcentral.com/jfp_submit and enter your Author Center, where you will find your manuscript title listed under "Manuscripts with Decisions." Under "Actions," click on "Create a Revision." Your manuscript number has been appended to denote a revision.
You will be unable to make your revisions on the originally submitted version of the manuscript. Instead, please upload your revised manuscript through your Author Center.
When submitting your revised manuscript, you will be able to respond to the comments made by the referees in the space provided. You can use this space to document any changes you make to the original manuscript. In order to expedite the processing of the revised manuscript, please be as specific as possible in your response to the referees.
IMPORTANT: Your original files are available to you when you upload your revised manuscript. Please delete any redundant files before completing the submission.
Because we are trying to facilitate timely publication of manuscripts submitted to the Journal of Functional Programming, your revised manuscript should be uploaded as soon as possible. If it is not possible for you to submit your revision in a reasonable amount of time, say two months, we may have to consider your paper as a new submission. Please let me know if this is not feasible.
Once again, thank you for submitting your manuscript to the Journal of Functional Programming and I look forward to receiving your revision.
Yours,
Benjamin
Dr. Benjamin Pierce
Journal of Functional Programming
bcpierce@cis.upenn.edu
Referees' Comments to Author:
Referee: 1
Comments to the Author
SUMMARY
This paper presents a polymorphic lambda-calculus equipped with references and
a region-based memory management discipline, in the style of Tofte and Talpin.
Safety is guaranteed by a type-and-effect discipline. Regions have lexical
scope, that is, they are organized in a stack. The system offers a standard
typing rule for region allocation & deallocation (with "effect masking"). It
also offers a somewhat lesser-known rule, known as "region extension", where
the newer region is not de-allocated, but instead merged into an older region.
The paper contains a formal definition of the system and a proof of type
soundness, based on preservation and progress lemmas. The definitions and
proofs have been mechanically checked using Coq.
EVALUATION
In favor of the paper, I found it rather easy to read, and I found the
definitions and statements reasonably natural and unsurprising. The static
semantics (figure 4) and the dynamic semantics (figure 6) are "what you would
expect", which I think is good. Some of the later figures (9, 10, 13) encode
internal invariants which certainly are more difficult to come up with, but
overall, the type system seems quite natural. Together with the Coq scripts,
this makes this paper an excellent reference for people interested in studying
the meta-theory of type systems based on a stack of regions.
That said, a few aspects of the paper I found somewhat disappointing.
For one thing, the motivation for this work, or the context in which this work
is taking place, are not really described. The author suggests that perhaps
this type system could be used (as a surface language? as an intermediate
language?) in a certified compiler for a functional language. Is this just a
suggestion, or is the construction of such a compiler actually being
considered or undertaken? The reason why I have some doubts is that the system
appears quite limited in expressiveness -- which is my next point.
It is well-known that purely stack-based region disciplines are too coarse.
They tend to force regions to remain live longer than necessary, effectively
causing memory leaks. Researchers have discussed ways of relaxing this
restriction quite early (e.g. Aiken et al., PLDI 1995). Attempts to use
regions in real-world programming languages, such as Cyclone, have proposed
many subtle mechanisms that help improve expressiveness. Also, systems based
on capabilities (linear or affine tokens, which represent the ownership of a
region) have appeared. Some of these systems have quite simple and beautiful
meta-theory (e.g. Ahmed et al., "L^3: a linear language with locations",
2007). I am sure the author is aware of these works, but my question is, why
not adopt one of these flexible type disciplines? They subsume the
stack-of-regions approach; they are not necessarily more difficult to prove
correct; they are much more expressive, and potentially more amenable to
unanticipated extensions. Here, the system is in some ways ad hoc: for
instance, a notion of "unique ownership" of regions seems to be implicit in
the typing rules TfConsPriv and TfConsExt of figure 10, but it is restricted
to the idea that "regions are uniquely owned by the stack", whereas in more
modern calculi, the notion of unique ownership is much more explicit and plays
a much more central role. The typing rule TxPrivate, although standard, also
seems somewhat limited: it relies on the absence of the region variable "r" in
the type "t" to ensure that "r" will not be accessed after it has been
de-allocated; but it seems to me that this wouldn't work any more if the
system was extended with existential quantification over regions, for
instance.
A (minor) detail that troubles me is that the author interprets \Lambda as
suspending evaluation, which in my opinion amounts to imposing a strong form
of the value restriction: it is essentially equivalent to requiring that the
body of every \Lambda be a \lambda. Yet, the author does not explicitly
acknowledge this (page 13). I would suggest at the very least clarifying the
situation. More ambitiously, one could view \Lambda as *not* suspending
evaluation, and (I believe) one could allow the body to be any expression
that does not have an Alloc effect. (Am I correct?) *That* would be a version
of the system without the value restriction.
I should also say that the whole of section 1.6 seemed somewhat unclear to
me. It wasn't really clear to me what the "problem" was, and the sentences of
the form "we could perhaps [fix the problem in this or that unlikely manner]"
were not helpful at all. As far as I am concerned, presenting the type system
as it stands, directly, would be preferable.
In summary, I would suggest accepting the paper for publication, on the
grounds that it is a solid, and one might even say tasteful, piece of work.
It is however somewhat unexciting, as the stack-of-regions discipline is a
20-year old idea, and there have many interesting developments since. It is
not clear that this discipline would have sufficient expressiveness for use
in the certified compiler project alluded to by the author in the conclusion.
As a reader, one would like to know more about this project.
MISCELLANEOUS REMARKS
p.3, "To ensure that further evaluation [...] the bound region variable r is
not free in the type of body." It seems that, if the type system were extended
with certain features, then this requirement would no longer be a sufficient
condition to ensure safety. For instance, what if existential quantification
over regions was added? It would then be unsafe to return a function of type
"exists r, Nat -(Write r)-> Nat" out of a "private" construct, even though the
type of this function is closed. Would the author care to comment on this
issue?
p.6, using "x" to denote an expression is non-standard and somewhat
mischievous. The author must be well aware that it usually denotes a variable.
p.6, "Now, although [...] we must deal with subtle issues [...]". I believe
that the paragraphs that follow are slightly misleading. The reader may be
led at first to believe that this is a hygiene (or name capture) issue, and
that "alpha-converting p" will fix the problem. Yet, (as the author points
out,) the *private* construct is not a binder, and the identifier p is not
a variable, so the name p in "*private* p" cannot be renamed; it is a fixed
name. The author presents a couple of "problematic" terms:
*private* p in *private* p in ...
(\Lambda r.*private* p in ...) (rgn p)
In what way are they "problematic", and what is the answer to these
"problems"? The answer is not that we need a special notion of renaming, or a
special notion of capture-avoiding substitution, or something like that. The
answer is simply that there is no "problem" and that these terms must somehow
be considered ill-typed. (That is, if my understanding is correct!) Perhaps
this could be clarified. It would be useful to point out, as soon as possible,
that *private* p does not bind p. In fact, ideally "*private* p in e" should
be written "e then dealloc p", which would more clearly suggest that this is
not a binding construct.
p.7, "In this work they give the following typing rule": is that (useregion)
on page 208 of Calcagno et al.'s paper? Please provide a more precise pointer.
p.7, "Now, [...] to add [...] polymorphism [...] we must deal with the capture
problem." At this point, I am not sure what the "capture problem" is, or why
there is a connection between polymorphism and this problem. By the way, it
occurs to me that when one discusses polymorphism in the presence of mutable
state, one should also discuss how one plans to control their interaction.
Adopting the value restriction is the simplest approach. It means that
evaluation never takes place under capital-Lambda. Here, since *private* is a
construct that appears only during evaluation, this means that *private* is
never nested under capital-Lambda; hence the term at the bottom of page 6 is
artificial and should never appear (it should be ill-typed). Also, this means
that the types and effects that occur in the typing rule TyPrivate are closed
(they do not have any free type variables). Doesn't this simplify the
"problem" (whatever the problem is!) in some way?
p.8, "The counter-example above is really a problem with [...]". It seems to
me that the whole thing is a problem of setting up the syntax and the typing
rules in such a way, that, together, they express the invariant that the
author has in mind. Anyway, as a reader, I do not appreciate the value of this
whole discussion; why not just present its solution directly?
p.8, "there is never a need to substitute types into it". This seems
consistent with my intuition that *private* should not appear under
capital-Lambda, hence one should never have to substitute types into it.
p.10, "We index environments from the right so that they appear as stacks that
grow to the left." Do you mean "that grow to the right"? In the typing rules,
new bindings seem to be added on the right-hand end of environments. (And that
is standard.)
p.10, "the store properties records the identifiers of regions that have been
created so far". This is fine, but as you note on p.18, one could just as well
replace the store properties (a set of identifiers) but just one integer
counter, namely the number of the next available region identifier. Is there
any reason not to perform this simplification?
p.12, "Rule (KiApp) prevents [...]". Couldn't one remove the restriction in
(KiApp) and instead require the primitive type constructors to have a kind
other than Region as their codomain?
fig. 2, (KiCon1) and (KiCon2) seem redundant with (KiApp), since both concern
type applications. Couldn't one just remove (KiApp)? After all, in System F,
type constructors are usually fully applied. Or if one wishes to go the other
route, keep (KiApp), but remove (KiCon1) and (KiCon2).
I would suggest grouping the components "se" and "sp" together in the typing
judgement. Together, they form a description of the "machine state" (they
describe which regions and which memory locations have been allocated,
together with certain invariants such as the type of every location). All
typing judgements are stable under an evolution of this "machine state"
according to a predetermined relation (allocating new regions, allocating new
regions). In this view, Lemmas 3.10 and 3.11 would become just one lemma. In a
sense, this would be just an aesthetic change; yet, it would also shed a
slightly more abstract light on the system, and help emphasize its similarity
with certain abstract frameworks in the literature: I am thinking of the Views
framework by Dinsdale-Young et al. (POPL 2013) and of the Mezzo kernel, as
presented by Balabonski et al. (FLOPS 2014).
fig. 4, rule TvLAM, I am slightly surprised to see that the store typing "se"
must be lifted in the premise. I would expect se to contain closed types only,
so that se is equal to its lifted version anyway. I suppose this appears
elsewhere (fig. 8), so it is only a matter of preference whether "se" or "se
lifted" is used in TvLAM.
According to TvLAM, a capital-Lambda-abstraction is a value, even if its body
is an expression. Thus, you have a non-type-erasure interpretation of
capital-Lambda: \Lambda suspends execution. Why is that? The type erasure
interpretation of \Lambda is more expressive, as one can still write
\Lambda\alpha.\lambda().x when one wishes to suspend evaluation, and one
potentially has access to \Lambda\alpha.x, which does not suspend evaluation
of the expression x, whereas your interpretation cannot express this.
As a related note, I believe that the paragraph "We require the body of a type
abstraction to be pure" (p. 13) is misleading in several ways. By deciding
that \Lambda suspends evaluation, you are effectively adopting a strong form
of the value restriction: in type-erasure terms, you are restricting the body
of a capital-\Lambda to be a little-\lambda, whereas the value restriction
usually allows the body of a capital-\Lambda to be any value (e.g., an empty
list constructor). Furthermore, the issue of "requesting the body of a type
abstraction to be pure" is an orthogonal problem altogether; you could allow
the body to have an effect, but that effect would have to be reflected in the
type, and your syntax does not allow a \forall type to carry an effect
annotation (it could). The bottom line, in my opinion, seems to be: 1- you are
effectively enforcing a strong value restriction, and you should say so; 2-
adopting a type-erasure interpretation of \Lambda would in my opinion be more
natural, more expressive, and would clarify some of these aspects.
p.15, in (TxPrivate), is the premise "t' = lower(t)" equivalent to
"lift(t') = t"?
The latter would seem more natural to me. Because lifting is a total function,
whereas lowering is a partial function (as emphasized by the author), it is
more common to reason purely in terms of lifting.
Why is Lemma 3.5 important? In a system with subtyping or sub-effecting, it
would be false. One would like this property not to be necessary. By the way,
why doesn't the system have sub-effecting? Wouldn't that make it more
expressive?
fig. 10, it is slightly surprising that TfConsExt needs stronger premises than
TfConsPriv. My intuition is that "private" and "extend" are almost the same
construct, except one de-allocates the region at the end, while the other
merges it into another region. So, the invariant that holds while the body is
evaluated should be the same. If the rule TfConsPriv was strenghtened by
replacing the NoPrivFs premise with FreshFs(Supp) premises, I assume the proof
would still go through?
p.33, "To achieve this, the CL requires programs to be written in CPS". It is
not clear to me that CPS is *required*. Walker et al. choose CPS style because
it is natural for a low-level language (such as a typed assembly language),
but one can also define a high-level, direct-style lambda-calculus and equip
it with affine capabilities (see Ahmed et al.'s L^3, or Tov and Pucella's
Alms, or Balabonski et al.'s Mezzo) which allow non-lexically-scoped
allocation and deallocation.
p.33, which "well known program transformations do you have in mind"?
TYPOS
p.3, "and so on a place-holder" -> "and so on as a place-holder"?
p.23, "the effect e being flattened" -> "the effect e is being flattened"?
p.28, "the effect if the initial state" -> "the effect of/in the initial state"?
p.36, the title of Papakyrakiou's paper is missing a \lambda.
p.34, "while it destructing it"
Referee: 2
Comments to the Author
This paper describes a formalisation of a type-and-effect system for
region-based memory-management for a system-F-like language extended
with mutable references. The paper presents a formalisation of a
static type-and-effect system for the language, a dynamic semantics
for the language, and a proof of type safety for the language. The
novelty of the paper is that the approach taken in the paper allows
type safety to be proven using standard small-step operational
semantics techniques even in the presence of mutable references and
polymorphism.
Overall, the paper is well-written, with only a few typographical
errors. However, at least one important issue needs to be addressed
before the paper can be published. In its current form, I believe the
type-and-effect system is incomplete in a significant sense: Due to
serial limitations in the type-and-effect system, many trivial
programs cannot be represented and typed in the type-and-effect
system. In particular, the type-and-effect system does not have a
sub-effecting rule and it does not support subtyping (with
sub-effecting on arrows), one of which is a requirement for giving a
type to a conditional expression with branches consisting of functions
with different effects. An alternative, which was used in the original
region-and-effect type-system by Tofte and Talpin, is to associate
each arrow effect with a particular effect variables, which, together
with a special-engineered substitution-operations would allow for the
unification of arbitrary effect- and region-decorated types, as long
as the underlying non-decorated types are identical. It is unclear to
the reader whether such a drastic change to the type-and-effect system
will require essential changes to the formalisms and to the proof of
soundness for the language. The paper should address this issue and
also compare a solution based on the substitution approach to unifying
effect types to using a subtyping approach.
The paper distinguishes between read effects and write effects (writes
to a mutable reference). Adding this distinction to the
type-and-effect system, which complicates proofs and adds complexity,
seems dual to the goal of proving type-safety for a region-based
language with support for mutable references and polymorphism. I would
suggest that the complications of the added generality is moved to a
separate section.
Details:
Page 4: Has the "region extension" technique been investigated in
isolation somewhere? Is it a contribution? If not, please add a
reference, and perhaps think about excluding it from the general
presentation (see above).
Page 5: "...construct not mention..." -> rephrase
Page 6: Syntactically, the vertical bar (|) seems to bind weaker than
turn-stile (|-) - using semicolon instead, could perhaps improve the
readability of lemmas...
Page 8: The solution to the renaming you're mentioning seems like the
obvious solution and doesn't seem like a "kludge" to me; as you say,
in an implementation, this sort of alpha-renaming would of course not
be done for real.
Page 9, Fig 1: The language supports booleans, but no conditional
expressions. Please consider adding conditional expressions, as such
an addition would shed light on many aspects of the effect system.
Page 10: "values are the expressions that cannot be reduced
further..." -> is "tt + 5" a value or a stuck expression?
Page 10: "that location is in" -> "that the location is in"
Page 12: "when adding allocating a" -> rephrase
Page 12: "and end of an" -> "and the end of an"
Page 14: Define maskOnVarT formally, or maybe refer to an appendix
with the proper definition and worked out properties.
Page 17: "we write it with in prefix" -> rephrase
Page 18: "takes the maximum of all existing region identifiers and
adds one to it" -> all existing as in ever created? Please clarify.
Page 21: There are many relations and objects to keep track of. It
would perhaps be beneficial to the reader if the objects could somehow
(syntactically or conceptually) be separated into those that are part
of the static semantics and those that are objects related to the
dynamic semantics.
Page 23: "will only accesses" -> "will only access"
Page 23: "preserved under during" -> "preserved during"
Page 23, Lemma 4.6: rephrase intro-text
Page 23: Please define regionOfStBind and handleOfEffect before use.
Page 23: "the rule (LiveE) rule" -> rephrase
Page 25, Fig 9: Should "p_1 with v |-_{bp} p_2 live" be "p with v
|-_{bp} p live" ?
Page 25 (and elsewhere): Use roman font for the turn-style subscript
text to avoid confusion with objects (effects, e.g.).
Page 29: "when apply rule" -> "when applying rule"
Page 30: "from to show" -> rephrase
Page 32, Theorem 4.2: Define "done fs x"
Page 32: "over the form of x" -> "over the structure of x"
Page 34: "while it destructing it" -> rephrase
Page 34: "not as memory management discipline" -> "not as a memory
management discipline"
Referee: 3
Comments to the Author
Title: Mechanized soundness for a type and effect system with region deallocation
Author: Ben Lippmeier
The paper considers an effect system a la Talpin and Jouvelot, that is, call-by-value lambda calculus with references and with type and region polymorphism. It gives a syntactic type soundness proof for the system, which is completely mechanized using the Coq proof assistant. The paper's approach is inspired by an earlier proof for a system with monomorphic types, which is not straightforwardly extensible to a type-polymorphic system.
The paper and the proof are carefully structured and the author worked hard to make a mechanized proof accessible in writing. The problems solved by the system are well presented (except my disagreement with region extension) and the paper is generally well written and accessible. Related work is also surveyed extensively.
However, the formalization contains some unfortunate decisions and in particular the fix to extend the previous monomorphic formalization makes the system unnecessarily complex. In particular, instead of considering a small-step semantics the author proposes a more complicated abstract machine semantics - this should not be necessary as Danvy has shown.
Given that the formalization is not particularly elegant and that there are already a number of (hand-written) proofs in the published literature and at least one of them (CL) covers a language with features very close to the author's System-Fre, it is hard for me to get excited about the paper. The author mentions the consideration of region extension as a contribution, but technically this is a minor extension which does not create new problem (nice to see, but unsurprising). This leaves the construction of the Coq formalization and proof as the main contribution.
This paper falls in the category "not embarrassing to accept" after a revision that addresses the points raised below, but leaving the abstract-machine style semantics as it is. But the archival value is not high as the proof is likely to be superseded.
DETAILED EVALUATION:
One difference to published systems is the consideration of region extension (section 1.4), which creates a new region, works with it, and then hides the resulting effect and merge the new region into an existing one. The main motivation of the author is that "Region extension allows store objects to be destructively initialized without revealing the associated write effects to the calling context". I fail to be convinced that this is a desirable property.
A programmer would more concerned that such a program part is able to willy-nilly change objects in an existing region. However, this encapsulation may also be achieved using region polymorphism:
Replace
extend r1 with r2 in x
by
(\Lamba r2:Region . x) r1
Of course, all the effects of x appear as effects of r1, but thanks to parametricity x cannot access or modify r1 objects unless they are passed explicitly (this is also possible with extend).
In Section 1.6, the author explains that the operational semantics is going to manipulate types. As previous work, for instance by Walker and others, has shown, it is possible to use actual values as region pointers. Type passing makes the impression that somehow types are needed at run time, which they are not.
In my opinion, the discussion of *private* is quite overblown. First, as also noted by the author, the offending expression is not reachable from any useful initial state of the system. Second, the proposed fix should clearly be that the offending expression is not well typed and then you would want the cheapest way of doing so.
On page 7, the author mentions that "region identifier ... are treated as constructors ... rather than variables" meaning that they are not subject to alpha renaming. As Harper explains in his book, this is the correct view: they stand for store addresses that are a-priori fixed and cannot be renamed.
In Figure 1 (page 9), I find it highly disturbing that variables are categorized as values with the explanation (page 10) "Values are expressions that cannot be reduced further". This is wrong and leads to underclassification later in the paper: whenever a lemma states "exists v such that ..." then v might be a variable.
Reynolds called this kind of expression "trivial expressions" because their evaluation has no effect.
Values are also trivial expressions, but they are further pinning down the possible outcomes of a computation.
I am also not sure whether it is a good idea to have big lambda as a value in a call-by-value calculus. For example, the capability calculus CL has just one abstraction which includes types and at least one value. This construction avoids intermediate values that are not observable in a call-by-value evaluation.
Again, I'd like to see a compelling reason for having types in run-time expressions.
Furthermore, it should be mentioned that this syntactic structure is A-normal form.
In Figure 2 (page 11), I don't understand the need for the specialized kinding rules KiCon1 and KiCon2 in particular given the ternary constructor (->) which is classified as a TyCon0. I'd also recommend dropping the restriction in the KiApp rule and enforce the invariant needed for the canonical forms lemma by restricting the available kind constructors.
Page 12: "We have not thought of a situation ..." that sounds weird and is a very weak, subjective statement.
I do not understand the proof engineering argument about KiCon0-KiCon2. You do get extra kinding rules, namely KiCon1 and KiCon2...
A general comment on the way that the lemmas are presented:
The statement of the lemma should be between "Lemma" and the \Box. But nothing else. The comments that are typeset inside almost every lemma and theorem have to go after the \Box.
In Lemma 3.1, don't we need p \in sp?
In Lemma 3.3, don't we need p \notin sp?
If not, why not?
Also, considering Figure 6 / page 9 rule (SfPrivatePush), it is strange that this push operation in the dynamic semantics is not reflected in the static semantics.
In Figure 8, I was puzzled first by the |-b judgment. In particular, it does not make sense that the store bindung has a reference type:
p with v :: Ref (rgn p) t
I see that this fits correctly with the neds of the (StoreT) rule, but I find the use of :: (which I read as "has type") irritating because elsewhere in the system an index into the store (i.e., an address) has the same type.
I suggest to another symbol instead of ::.
In Lemma 4.6, page 23, you find an example for the underclassification that I mentioned above.
The last line says "exists v. b = p with v" where v is certainly not a variable.
BTW I was not able to locate an explanation for the notation "v". The grammar says "val".
Lemma 4.8: The typesetting of "priv m p" and "rgn p" is incorrect. Same in Lemma 4.9 with "priv d p"and "(NoPrivFs p fs)".
Section 4.4, page 25. Is the use of the lolli symbol -o justified? It is customarily used for linear function space and you should argue that this is also a linear function space.
Section 4.5: it seems to me that some of the difficulties in dealing with effects (i.e., that they grow and shrink) and the complexity arising in managing that is also due to the formulation as an abstract machine, where the current focus of the computation is exposed. It should not be an issue in a proper small-step semantics.
Page 34: Morisett -> Morrisett
References, page 35.
It is disappointing that very many references are incomplete. Almost all conference papers are cited without page numbers; the LNCS volumes without mentioning the publisher, LNCS, and the volume number; also the conference locations are missing.
* SIGPLAN Notices is not correct for Fahndrich and DeLine (which should be F{\"a}hndrich btw): it is a PLDI paper.
* Chung Chieh Shan 's name is permuted
* Pena should be P\~{e}na
* Andr{\'e} Santos
There is also an early published paper by Gifford and/or Lucassen at LFP 1986, not just the techreport.