## A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions

A Type-theoretic Foundation for Programming with Higher-order Abstract Syntax and First-class Substitutions by Brigitte Pientka, appeared in POPL 08.
Higher-order abstract syntax (HOAS) is a simple, powerful technique for implementing object languages, since it directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. This is achieved by representing binders in the object-language via binders in the meta-language. However, enriching functional programming languages with direct support for HOAS has been a major challenge, because recursion over HOAS encodings requires one to traverse - abstractions and necessitates programming with open objects.

We present a novel type-theoretic foundation based on contextual modal types which allows us to recursively analyze open terms via higher-order pattern matching. By design, variables occurring in open terms can never escape their scope. Using several examples, we demonstrate that our framework provides a name-safe foundation to operations typically found in nominal systems. In contrast to nominal systems however, we also support capture-avoiding substitution operations and even provide first-class substitutions to the programmer. The main contribution of this paper is a syntax directed bi-directional type system where we distinguish between the data language and the computation language together with the progress and preservation proof for our language.

Its been a while since I posted, but this paper appears that it may be of interest to some members of this community. It looks interesting to me, but I just wish I understood all the terminology. I don't know what "open objects" are, and why they are a problem. I don't understand what HOAS is. I don't even know what binders are. The list goes on. I surely can't be the only person who is interested, but feels that this is just out of their grasp. I bet that I probably could understand these things with a minimum of explanation, given I have experience implementing languages. If anyone is interested in rephrasing the abstract in more basic terms, I would be very appreciative. [Edit: corrected spelling of Brigitte Pientka. My apologies.]

## Comment viewing options

### For a programmer, "abstract

For a programmer, "abstract syntax" is a datatype describing expressions in a programming language. For example, in Ocaml, we might have a datatype declaration like the following for the syntax of the pure lambda calculus:

   type var = string

type exp = Var of var | App of exp * exp | Lam of var * exp


This is straightforward, but when you try to implement operations -- like substitution -- on this datatype, you find yourself having to do all the usual things like rename variables to avoid variable capture. gThis is a medium-sized pain in the butt when doing an implementation, and it becomes a large-ish pain in the butt when doing a correctness proof, because all your theorems have to be stated modulo all this renaming business, and any recursive functions on syntax has to prove that renamings won't change the answer in any important way, and so on. There's nothing terribly hard here, but there's a lot of tedious formality which distracts people from the real meat of your ideas.

So a few decades ago, people came up with the idea of "higher-order abstract syntax". The idea was that whatever language you were using had already implemented substitution, so why not just reuse that? Then we can get substitution and so on for free, just by reusing the work that the implementor of our meta-system had already done. So a HOAS representation of the untyped lambda calculus might look like

  type exp = App of exp * exp | Lam of (exp -> exp)


Now, you can represent variable binding using the lambda-abstraction of Ocaml, and represent variables using Ocaml variables. So the omega-combinator could be written as follows:

  (* omega is the looping combinator, (\x. x x) (\x. x x) *)

let omega = App(Lam(fun x -> App(x, x)),
Lam(fun x -> App(x, x)))


Notice that we are using Ocaml functions to represent variable abstraction in the language we're implementing (ie, the untyped lambda calculus). The language we're implementing is called the "object" language, and Ocaml is our "meta" language. So the strategy of HOAS is "represent object-level variables and abstractions with meta-level variables and functions".

Of course, we are not immediately in the land of milk and honey.

To pick just one example, it's easy to represent closed terms with HOAS, but what about open terms -- that is, terms with free variables in them? These come up very often both in theory, and in compiler implementations (for example, a simplification pass which turns expressions "x + 0" into "x" needs to work on open terms). One thing we can do is to represent free variables with more Ocaml lambda-abstractions. For example, an object term with a single free variable might be represented with a term of Ocaml type exp -> exp:

  (* A term with one free variable:  \x. x y *)

let onefree = fun y -> Lam(fun x -> App(x, y))


However, this is not an approach that readily scales, for two reasons. First, the type we need depends on the number of free variables. With one freevar, we have  exp -> exp; with two,  exp -> exp -> exp, and so on. The second problem is that we need to analyze open terms (for example, suppose we need to compute the size of a term with a free variable), and the only thing we can do with function types is to apply them!

There's a long history of various approaches to deal with these issues, but the one that's used in this paper is to use a "contextual modal type theory". The idea is to introduce a type [Γ] exp  (pronounced "box gamma exp"), which says that we have a term of type exp, with free variables listed in a context Γ. (The idea is to view types relative to a variable context, from which the terms "contextual" and "modal" come from.)

So our earlier example could be given the type [y:exp] exp, which says that it is a term of type exp, assuming that we have an extra free variable y of type exp occurring inside it.

  (* A term with one free variable:  \x. x y *)

let onefree : [y: exp] exp = Lam(fun x -> App(x, y))


Then there's a bunch of machinery to let you manipulate these terms with free variables (ie, open terms) without any variables escaping their scope or accidentally getting captured and breaking the alpha-conversion rules we expect to hold.

As an aside, I've omitted a LOT of issues in this brief discussion -- I tried to cover only enough to decode the abstract. Variables are a surprisingly rich subject (irritatingly complex, if you're actually interested in something else!)

### HOAS, the very idea

So a few decades ago, people came up with the idea of "higher-order abstract syntax"

To get slightly historical, the basic idea behind HOAS is Church's work on representing quantifiers using lambda abstraction, which essentially is the origin of the lambda calculus. I'd say that van Dalen's work on Automath is the first HOAS work, in that it studies the general application of this intuition.

### Great post, Neel. Thanks.

Great post, Neel. Thanks.

### Thank you!

Thank you very much Neel, this is This is the kind of post that is going to be a great resource for newcomers, and non-theorists like myself for a long time coming.

So as I understand it this kind of theory is very important for people trying to implement languages using a formal approach. E.g. implementing the language using a small formal meta-language.

It seems like this is a very different approach then the one used by thousands of hackers like myself who just bolt together programming language implementations in some general purpose programming language. I can make a language implementation work, more or less, but I may never be able prove that there are no bugs.

By the way, I read your post three times and I got something new out of it each time. You have a talent at making a very rich and complex subject very accessible!

### What's the use?

This sort of theory is potentially useful to anyone implementing languages related to the lambda calculus (at the very least). Presumably they have to do at least some manipulating of abstract syntax, and want correct implementations of alpha conversion, and possibly even beta reduction and such. Even the abstract machine language for the STG machine has variable names, for instance.

It's not impossible to just work with (string) variable names, and get everything correct. However, it's easy to make mistakes; especially so if you're doing some sort of code generation that needs to make up fresh names. For instance, in their paper I am not a Number, I am a Free Variable McBride and McKinna talk about generating inductive elimination principles in some type theory. One example they use is:
 data Nat = Zero | Suc Nat 
and want to generate the eliminator type:
 ∀(P : Nat → Prop). P Zero → (∀(k : Nat). P k → P (Suc k)) → ∀(n : Nat). P n 
But, you have to be careful in doing so, not to accidentally do:
 data P = Zero | Suc P

 

elim : ∀(P : P → Prop). P Zero → (∀(k : P). P k → P (Suc k)) → ∀(n : P). P n 
So, your code generator needs to be robust enough not to pick names that are already in use.

There are several schemes for circumventing this sort of issue. For instance, De Bruijn indices/levels use natural numbers instead of names for bound variables, so for the above, you get something like:
 ∀(Nat → Prop). 0 Zero → (∀Nat. 1 0 → 1 (Suc 0)) → ∀Nat. 1 0 
HOAS is another solution. The practical side of all this is that you don't have to implement the error-prone munging of variable names. Why write and check code for that when you can use some other technique that doesn't need it, and lends itself toward your writing the right code from the start? Of course, other techniques have their own trade-offs. But this isn't just a purely theoretical exercise.

HOAS also has connections to embedded DSLs in languages like Haskell. As an overly simplified example, presentations of delimited continuations sometimes present shift as a new sort of binder:
 shift k in <k can be referred to here> 
But one can obviously make shift higher-order instead:
 shift (\k -> ...) 
So, EDSLs (by necessity, I suppose, in the Haskell case) implement binders for the DSL as binders in the meta-language, just like HOAS.

### de-Bruijn-like approaches

You reminded me of another line of work, which goes back to work of Andrew Gordon. Cf. Gordon and Melham (1996), Five Axioms of Alpha-Conversion, LNCS 1125:173-190.

The basic approach is come up with an axiomatisation of what a theory needs to satisfy for its names to be free of substitution issues, and then prove that whatever concrete representation you want to use satisfies this property. The paper does this for the de Bruijn representation. I seem to recall that Andrew Pitts said that the technique wasn't completely straightforward in its application, but I don't recall what the problem was.

Another point is that the de Bruijn representation has a nontrivial parallel to the implementation of closures: lambda abstractions are like frames, and de Bruijn indices are a count of how many times you need to hop into the next-most enclosing frame to get to the one that binds the correct variable.

### I think I understand 'box gamma exp'

[Edit: upon rereading the paper, I can that this comment, really misses the mark. Contexts are not as simple as that. I'm going to leave it for the sake of amusement. :-)]

I think I understand box gamma exp. A context is essentially a dictionary, right? Mapping names to values. So what I am understanding here is the suggestion that a term with free variables (e.g. a closure) can be implemented (at the meta-level) by using a dictionary meta-type. Right?

This seems kind of common sense doesn't it? This is exactly how I implemented closures in my language (and I am guessing many other people do as well).

I guess the magic here, is being able to do it in a provably correct way in a meta-language. That seems like quite a feat.

### Not quite

An open term isn't quite the same thing as a closure. The difference is that a closure has a value associated with each variable, whereas an open term doesn't. The free variables are really just typed placeholders, with nothing bound to them (yet).

A better way to think of the context is as a list of variables names. If gamma lists the variables x and y, then (suc x), (suc y) and (x + y) all have type [gamma]nat, but (suc z) doesn't.

In addition to listing the variable names, a context also lists the types of those variables. So if gamma is {x:nat, y:list nat}, then (suc x) has type [gamma]nat, but (suc y) doesn't.

### On HOAS

You give this data type in OCaml for a 'HOAS' representation of the syntax of the lambda calculus:

  type exp = App of exp * exp | Lam of (exp -> exp)


This is not HOAS. It does not represent terms with binding; it is the solution of a particular recursive domain equation that contains pairs and functions. This data type contains many things that do not represent any lambda term, e.g.:

  let not_a_term = Lam (fun e -> match e with
| App (_,_) -> e
| Lam _     -> App (e,e))


This value in the type exp "represents" a lambda abstraction that has a different body depending on whether the closure representing the body is passed an application or a lambda. Such values in this type are called "exotic" terms.

It is possible to attempt to get around this by restricting when the programmer is able to pattern match on members of types one wishes to use for representing data with binders. This is the approach taken by Fergaras and Sheard in Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space).

A better solution, first proposed, to my knowledge, by Coquand and Huet in Constructions: A higher order proof system for mechanizing mathematics back in 1985 and later independently promoted by Washburn and Weirich in Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism, is to use parametric polymorphism. They use the type:

  exp = forall a. ((a -> a) -> a) -> (a -> a -> a) -> a


An example term is represented like so (explicitly writing the type abstraction):

  omega = /\a. \lam app. app (lam (\x -> app x x)) (lam (\x -> app x x))


The idea is that because the type a is kept abstract, it is not possible to analyse it and create exotic terms.

This is similar to the Church encodings of inductive data types (e.g. forall a. a -> (a -> a) -> a for the natural numbers): there is a universally quantified type variable for the carrier and a collection of "constructors" (abstraction and application for the exp type and zero and successor for the natural number type). The exp differs because there is a negative occurrence of a in the abstraction constructor, which is normally disallowed.

Neither Coquand and Huet nor Washburn and Weirich presented a proof that the exp type actually does represent only the untyped lambda calculus terms. I proved this in a TLCA paper published this year: Syntax For Free: Representing Syntax with Binding using Parametricity, in the setting of System F. One needs to use parametricity over Kripke logical relations to prove the result; the Kripke indexing is required to keep track of the number of binders that have been passed under. The paper also shows that weak HOAS (AKA Chlipala's "Parameterised HOAS") is isomorphic to normal HOAS, and that computational and syntax-with-binding can be intermixed easily (c.f. A universe of binding and computation by Licata and Harper). It also gives an interesting perspective on the Haskell ST monad (by thinking of dynamic allocation as name binding).

The construction at the core of the proof gives a way of going from the HOAS type exp to a more normal de Bruijn representation and back again. With Sam Lindley and Jeremy Yallop, we wrote a paper Unembedding Domain-Specific Languages that does this in Haskell and shows how one can use HOAS as an input language for EDSLs, but still retain the capability of converting to a de Bruijn representation which may be easier to work with. We also show how to do object languages with pattern matching and also how to represent open terms with arbitrary numbers of free variables, captured in the type system.

This technique extends smoothly to typed languages, using Haskell's types to represent types in the embedded language. This turns out to be very similar to Carette et al's "Finally Tagless" approach Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. We note in the "Unmebedding..." paper that to get an adequate representation of actual typed terms, one needs to restrict to a fixed subset of Haskell types rather than use all types as in the "Finally Tagless" approach, lest one allow "exotically typed" terms. Manuel Charavarty noted the same thing in his conversion from "not HOAS" to de Bruijn terms.

As a side note, I think that the "Finally" is pretty much meaningless here: the message of my "Syntax for free" paper is that the parametric polymorphic HOAS representation is actually a way of representing initial algebras in pre-sheaves (c.f. the Fiore, Plotkin, Turi approach to a mathematical representation of syntax with binding) just using parametric polymorphism, which is pretty cool.

I have recently been working on how to write computations over the parametric polymorphic HOAS (and weak HOAS) representations that gets some of the advantages of the new programming languages like the one presented in the paper at the top of this thread. I have been able to cover all the examples in this paper, plus some nice examples of NBE for various languages. I'll try and put them on-line sometime.

This is not HOAS. It does not represent terms with binding; it is the solution of a particular recursive domain equation that contains pairs and functions. This data type contains many things that do not represent any lambda term, e.g. ...

Yes, you are entirely correct.

I was deliberately trying to avoid talking about adequacy of representations, but I suppose that avoiding at the price of technical error is too high a price to pay!

Neel said:

I was deliberately trying to avoid talking about adequacy of representations, but I suppose that avoiding at the price of technical error is too high a price to pay!

Though as a community member I'd like to thank both Bob and Neel for their contributions to this thread, I'd like to take a contrary view to this quoted section as it relates to LtU discussions.

Sometimes when trying to help out with an issue of basic understanding about some topic, it is necessary to glide over some of the "gory details". Once the other person "gets it", then the gory details can come back in.

Professors do this all the time in intro courses, and this relates to the use of the discussion of pseudo-code in algorithms textbooks.

I think Neel's presentation was just right for the spirit of the thread, and if the other choices were to make the example too complicated to follow for the original poster, or to not post at all to avoid an inaccuracy of detail, I think the best option for LtU is exactly the one he chose, i.e. an informative approximation.

### Adequacy is a very modest

Adequacy is a very modest name for a vitally important question: does the data representation actually faithfully represent what we intend? So when we write down an abstract syntax, and represent it with a fancy data structure, we really need for there to be a one-to-one correspondence between the intended syntax and the elements of the representation.

The existence of "exotic terms" shows that the datatype I gave is NOT adequate -- there's weird stuff in the type that doesn't correspond to any syntactic object. This isn't an entirely theoretical concern, either -- you can make some Lisp compilers go into infinite loops by asking them to compile programs represented as circular lists. This can be viewed as the result of a failure of adequacy: the compiler is written expecting the type of s-expressions to be well-founded, but the data type actually includes infinite terms that the compiler writer didn't expect.

If there were no way to ensure adequacy with HOAS, the whole approach would be a non-starter, because we'd be throwing away what we wanted and using some random datatype instead. So Bob's objection is wholly justified; the fact that adequate representations are possible is a critical feature of the methodology of HOAS.

The LF type theory used in Twelf (and Beluga, the system of this post) is very carefully engineered to restrict the function type so that exotic terms do not occur, and to make adequacy proofs very easy. You can view the work of Fiore et al. as a way of giving a denotational semantics to (many?) LF types.

But though presheaf models are a sturdy workhorse of semantics, they do have the downside that translating them into type theory is a bit awkward (you move "up a level" when you model presheaves straightforwardly in type theory). So I think Bob undersells his own work somewhat when he calls his proof of the equivalence of parametric representations with presheaf models "pretty cool" -- it's actually really, really cool, because now you've got a program you can actually run to translate between representations. I highly endorse reading both of his (and his coauthors') papers he linked to. :)

### This is a great thread

This is a great conversation. I know its lame to say so, but I had to say it. I am able to start getting a hint of how things like exotic terms tie into implementation problems in a compiler. Its weird how a compiler implementor can run into these kinds of problems, without knowing a thing about how deep the theory is behind it.

### Expected outcome

Its weird how a compiler implementor can run into these kinds of problems, without knowing a thing about how deep the theory is behind it.

Actually, this is just what you would expect in a healthy subject domain: the theoreticians and the practitioners talking about the same things, just one in the abstract and general case, the other in the concrete and particular.

If practitioners never stumbled across issues of theoretical import in their practice, you would have to wonder about the health of the field. ;-)

The existence of "exotic terms" shows that the datatype I gave is NOT adequate -- <snip> This isn't an entirely theoretical concern

I understand the problem, and acknowledge that if the point of your post was to give a detailed recipe on how to implement HOAS, that flaw would be fatal.

If on the other hand, your goal was to answer the OP's question, and further the poster's understanding of the issue itself, the "flaw" is an incidental casualty of the explanatory process.

I think it is great that people like Bob make those of us who already have the background to understand the issues aware of their valuable work.

But for those who don't yet get the gist of the problem, it is helpful to understand the idea before we get bogged down in the tough spots.

My purpose in pointing this out is to use this as a "teachable moment". I've lost count of the number of times I've been in threads where what started as an attempt to give the yin-and-yang of a problem to a poster, or to clarify a misunderstood foundational issue, turns into a master-class quibble-fest.

It is a disincentive to those who want to help beginners in a particular subject from posting if every time someone does it, they get publicly spanked by the experts. ;-) Especially when it's not that they have made a mistake but rather that they have made a strategic simplification.

I think it is great that we have both advanced-level and beginner-level discussions here. I think we just need to be a little more discerning of which is which.

### I don't mind the

I don't mind the master-class quibblefest effect so long as it's clear where the transition lies and people aren't treated disrespectfully for giving beginner-level answers. Done that way, the thread ends up managing to teach a wider range of people.

Of course, spanking generally isn't respectful :-)

### The monsters of HOAS

This is not HOAS. It does not represent terms with binding; it is the solution of a particular recursive domain equation that contains pairs and functions. This data type contains many things that do not represent any lambda term

Morally speaking, you are right: HOAS is about appropriate representations of possible terms of some language with binders. As a criterion describing what the literature accepts and rejects as being HOAS, this is not right. Using function spaces that overgenerate in the way you describe is not rare.

I think the reason people are willing to tolerate overgeneration is something along the lines of: each term-with-binders has an obvious, canonical representation in HOAS, so the image of our alpha-challenged term calculus in HOAS provides us with the syntactic theory we need, and who cares about the monsters lurking in the dark?

### Fear of the dark

The problem with monsters lurking in the dark is that cannot safely retrieve anything from the dark. We push things in, and we are happy that they fit, but once they are in, we have lost them.

More concretely, the type that Neel gave:

  type exp = App of exp * exp | Lam of (exp -> exp)


has the serious bug that practically no useful functions can be written that take exp as input. For instance, maybe we want to write a function that computes the size of a term. So we try:

  let rec size t = match t with
| App (t1, t2) -> 1 + size t1 + size t2
| Lam t        -> 1 + size (t ???)


What do we put for ???? We need to pass in an exp, so we are limited to either App (...,...) or Lam ..., but either of these will lead to non-termination.

Fegaras and Sheard (see my other post above) solved this problem by adding a new constructor to represent whatever it was that was being computed, and parameterised everything by a type:

  type 'a exp = App of 'a exp * 'a exp | Lam of ('a exp -> 'a exp) | Hole of 'a


Now we can write the size function, but we still have the problem that exotic terms are representable (Fegaras and Sheard fix this by an ad-hoc extension to the type system to prevent case analysis of certain types). But we are nearly there! All we have to do is drop the negative occurrence of exp and wrap everything in a type abstraction:

  type 'a exp' = App of 'a exp' * 'a exp' | Lam of ('a -> 'a exp') | Var of 'a
type exp = { x : 'a. 'a exp' }


This is Chlipala's parameterised HOAS, previously known as weak-HOAS, and it represents all and only the untyped lambda terms, see my "Syntax for Free..." paper (modulo problems with non-termination (which I think gives you possibly infinite terms) and the non-parametric features of OCaml). We can now write the size function easily by instantiating the 'a to be int.

This is from the #haskell channel (thanks Saizan)

Inspired (copied) from the "Parametric Higher-Order Abstract Syntax for Mechanized Semantics" paper

untyped HOAS:

data Exp' a =
Lam (a -> Exp' a)
| App (Exp' a) (Exp' a)
| Var a

type Exp = forall a. Exp' a

data TExp' a b where
Lam :: (a b -> TExp' a c) -> TExp a (b -> c)
App :: TExp' a (b -> c) -> TExp' a b -> TExp' a c
Var :: a b -> TExp' a b

type TExp = forall a. TExp' a

### A minimal explanation

I haven't looked at the paper, but I can give some answers and another reference.

A binder
is a syntactic construct that introduces name which is lexically scoped, in the sense that the construct has an inside, where usages of have a consistent meaning, and an outside where that meaning of the name cannot directly be accessed. The paradigmatic examples are lambda abstractions, quantifiers in first-order logic, how the dx in Riemann integral binds the variable x, and variables in set comprehensions.
An open object
is an object that is represented by a term with variables outside the scope of any binder.
The problem with binders
arises when we want to do use structural induction to reason about them, and it results from alpha-equivalence. Infinitely many terms belong to each alpha-equivalence class, so terms-up-to-equivalence are not syntactic entities at all. The issue seems trivial, but it is amazing how much trouble it causes.
HOAS
is a particular approach to make the term language more tractable by reexpressing it using a metalanguage, in the case of HOAS, the lambda calculus. Nominal logic uses a different metalanguage that distinguishes variables from names, and has a quantifier to express the scope of variables based on a theory of name permutability.
I recommend Pitts (2006), Alpha-Structural Recursion and Induction, Journal of the ACM 53:459-506.

### Very useful glossary

This is a great mini-glossary Charles, thank you. It really helps to get a sense of what is being discussed and help orient me in the massive world of language theory. The fact that the problem with binders is in the context of "structural induction" is a really key point for me. If I never do structural induction, I probably will never want to know the theory at the level of detail used in the paper. It is also an interesting revelation that that I would have to understand structural induction if I ever want to reason about the language implementations I work on. The Pitts paper seems to be very thorough in its treatment of the subject of variable binding and alpha-equivalence, thank you.

Yes, reasoning about your language implementation will be another area where the "bound name problem" comes in. This motivates efforts like Nominal Isabelle, which aims to provide support for working with alpha-equivalence classes in Isabelle/HOL. See Christian Urban's poster, "How to prove false using the variable convention" for a demonstration of how insidious naive reasoning with binders and alpha-equivalence classes can be.

As Charles mentioned, there's a whole mini-industry trying to solve the name binding (and related) problems, with (markedly) different methods. HOAS, and its variants, are one approach, embedding object-languages inside the simply-typed lambda-calculus. Gabbay and Pitts' Nominal sets are another, and were the inspiration for FreshML, alpha-Prolog, Nominal Isabelle, etc. de Bruijn indices "solve" the problem by making alpha-equivalence checks coincide with textual equality, at the expense of readability for human users (if that's a concern). Locally nameless approaches are another approach, along with many others.

I hope the maintainers of LtU won't mind a bit of a plug, but I recently started a blog, in a similar vein to LtU, for discussing these matters related to name binding. Rather strangely, I posted this same paper on the blog a few days ago!

### a glossary for new comers

Thank you, Neel, Bob, and Charles. I think a glossary for new comers in PL research is long over due. PL research extends to so many fields, such as logic, type theory, category theory, etc., some of which easily date back to the 19th century. When there is so much knowledge behind it(that is why this field is so intriguing!), some research papers in this field are simply too overwhelming to read. Maybe LtU can start a Wiki so that we can work together on a glossary that is both theoretically correct and self contained?
p.s. I have long been a reader of LtU but never posted before. I apologize if this comment is irrelevant.

### A LtU-wiki is high on our

A LtU-wiki is high on our todo list. It will appear at some point, I promise.

### It exists

It can be used, at least in principle. However, it is not ready for general use. IIRC:

1. We have not really figured out the editorial policy yet. So anything you put there might not stay;
2. The wiki software is not yet unified with the main site, so there is no uniform login.