Higher-Order Dynamic Pattern Unification for Dependent Types and Records

Andreas Abel^{1} and Brigitte Pientka^{2}

1 Institut für Informatik, Ludwig-Maximilians-Universität, München, Deutschland

                         andreas.abel@ifi.lmu.de

2 School of Computer Science, McGill University, Montreal, Canada

                          bpientka@cs.mcgill.ca

Abstract. While higher-order pattern unification for λ^{Π}-calculus is decidable and unique unifiers exists, we face several challenges in practice:

1) the pattern fragment itself is too restrictive for many applications; this is typically addressed by solving sub-problems which satisfy the pattern restriction eagerly but delay solving sub-problems which are non-patterns until we have accumulated more information. This leads to a dynamic pattern unification. 2) Many systems implement λ^{ΠΣ} calculus and hence the known pattern unification algorithms for λ^{Π} are too restrictive. In this paper, we present a constraint-based unification algorithm for λ^{ΠΣ}-calculus which solves a richer class of patterns than currently possible; in particular it takes into account type isomorphisms to translate unification problems containing Σ-types into problems only involving Πtypes. We prove correctness of our algorithm and discuss its application.

1 Introduction

Higher-order unification is a key operation in logical frameworks, dependentlytyped programming systems, or proof assistants supporting higher-order logic. It plays a central role in type inference and reconstruction algorithms, in the execution of programs in higher-order logic programming languages, and in reasoning about the totality of functions defined by pattern-matching clauses.

While full higher-order unification is undecidable [7], Miller [8] identified a decidable fragment of higher-order unification problems, called the pattern fragment. A pattern is a unification problem where all meta-variables (or logic variables) occurring in a term are applied to some distinct bound variables. For example, the problem λx y z. X x y = λx y z. x (suc y) falls into the pattern fragment, because the meta-variable X is applied to distinct bound variables x and y; the pattern condition allows us to solve the problem by a simple abstraction X = λx y. x (suc y). This is not possible for non-patterns; examples for non-pattern problems can be obtain by changing the left hand side of the previous problem to λx y z. X x x y (non-linearity), λx y z. X (Y x) y (X applied to another meta-variable) or λx y z. X x (suc y) (X applied to non-variable term).

In practice we face several challenges: First, the pattern fragment is too restrictive for many applications and we want to solve more general problems incrementally. Systems such as Twelf [12], Beluga [14], and Delphin [15] solve eagerly sub-problems which fall into the pattern fragment and delay sub-problems outside the pattern fragment until more information has been gathered which in turn simplifies the delayed sub-problems. The meta-theory justifying the correctness of such a strategy is largely unexplored and complex (an exception is the work by Reed [16]).

Second, we often want to consider richer calculi beyond the λ^{Π}-calculus. In Beluga and Twelf for example we use Σ-types to group assumptions together. In Agda [10], we support Σ-types in form of records with associated η-equality in its general form. Yet, little work has been done on extending the pattern fragment to handle also Σ-types. The following terms may be seen as equivalent:

(a) λy_{1}.λy_{2}. X (y_{1}, y_{2}), (b) λy. X (fst y) (snd y) and (c) λy_{1}.λy_{2}. X y_{1} y_{2}. Only the last term falls within the pattern fragment as originally described by Miller. However, the other two terms can be transformed such that they also fall into the pattern fragment: for term (a), we replace X with λy_{1}.λy_{2}. X′ y_{1} y_{2}; for term (b), we unfold y which stands for a pair and replace y with (y_{1}, y_{2}).

In this paper, we describe a higher-order unification algorithm for the λ^{ΠΣ} calculus; our algorithm handles lazily η-expansion and we translate terms into the pure pattern fragment where a meta-variable is applied to distinct bound variables. The key insight is to take into account type isomorphisms for Σ, the dependently typed pairs: Πz:(Σx:A.B).C is isomorphic to Πx:A.Πy:B.[(x, y)/z]C, and a function f:Πx:A.Σy:B.C can be translated into two functions f_{1} : Πx:A.B and f_{2} : Πx:A.[f_{1} x/y]C. These transformations allow us to handle a richer class of dependently-typed patterns than previously considered.

Following Nanevski et al. [9] and Pientka [13], our description takes advantage of modelling meta-variables as closures; instead of directly considering a metavariable X at function type Πx:A.B which is applied to x, we describe them as contextual objects, i.e., objects of type B in a context x:A, which are associated with a delayed substitution for the local context x:A.^{3} This allows us to give a high-level description and analysis following Dowek et al. [2], but not resorting to explicit substitutions; more importantly, it provides a logical grounding for some of the techniques such as “pre-cooking” and handles a richer calculus including Σ-types. Our constraint-based unification algorithm also avoids some of the other shortcomings; as pointed out by Reed [16], the algorithm sketched in Dowek et al. [2] fails to terminate on some inputs. We give a clear specification of the pruning operation which eliminates bound variable dependencies for the dependently typed case and show correctness of the unification algorithms following Reed [16] in three steps: 1) we show it terminates, 2) we show that the transformations in our unification algorithm preserve types, and 3) that each transition neither destroys nor creates (additional) solutions.

Our work is to our knowledge the first comprehensive description of constraintbased higher-order pattern unification for the λ^{ΠΣ} calculus. It builds on and extends prior work by Reed [16] to handle Σ-types. Previously, Elliot [4] described unification for Σ-types in a Huet-style unification algorithm. While it

3 We write x:A for a vector x_{1}:A_{1}, … x_{n}:A_{n}.

is typically straightforward to incorporate η-expansions and lowering for metavariables of Σ-type [18, 11], there is little work on extending the notion of Miller patterns to be able to handle meta-variables which are applied to projections of bound variables. Fettig and Löchner [5] describe a higher-order pattern unification algorithm with finite products in the simply typed lambda-calculus. Their approach does not directly exploit isomorphisms on types, but some of the ideas have a similar goal: for example abstractions λx. fst x is translated into λ(x_{1}, x_{2}). fst (x_{1} , x_{2}) which in turn normalizes to λ(x_{1}, x_{2}).x_{1} to eliminate projections. Duggan [3] also explores extended higher-order patterns for products in the simply-typed setting; he generalizes Miller’s pattern restriction for the simply-typed lambda-calculus by allowing repeated occurrences of variables to appear as arguments to meta-variables, provided such variables are prefixed by distinct sequences of projections.

Our work has been already tested in practice. Some of the ideas described in this paper are incorporated into the implementation of the dependently-typed Beluga language; in Beluga, Σ-types occur in a restricted form, i.e., only variable declarations in contexts can be of Σ-type and there is no nesting of Σ-types.

Due to space restrictions, most proofs have been omitted; they can be found in an extended version of this article on the authors’ homepages.

2 λ^{ΠΣ}-calculus

In this paper, we are considering an extension of the λ^{ΠΣ}-calculus with metavariables. Meta-variables are characterized as a closure u[σ] which is the use of the meta-variable u under the suspended explicit substitution σ. The previous term λx y z. X x y with the meta-variable X which has type Πx:A.Πy:B.C is represented in our calculus as λx y z. u[x, y] where u has type C[x:A, y:B] and [x, y] is a substitution with domain x:A, y:B and the range x, y, z. Instead of an abstraction, we can directly replace u with a closed object x, y. x (suc y). This eliminates the need to craft a λ-prefix for the instantiation of meta-variables, avoids spurious reductions, and provides simple justifications for techniques such as lowering. In general, the meta-variable u stands for a contextual object Ψ̂.M where Ψ̂ describes the ordinary bound variables which may occur in M. This allows us to rename the free variables occurring in M if necessary. We use the following convention: If the meta-variable u is associated with the identity substitution, we simply write u instead of u[id]. A meta-variable u has the contextual type A[Ψ] thereby characterizing an object of type A in the context Ψ. Our grammar and our subsequent typing rules enforce that objects are β-normal; this will simplify the later development.

The grammar is mostly straightforward; a signature Σ is a collection of constant declarations, which take one of the forms a : κ (type family declaration) or c : A (constructor declaration). Because variable substitutions ρ play a special role in the formulation of our unification algorithm, we recognize them as a subclass of general substitutions σ. Identity substitutions id_{Φ} are defined recursively by id_{·} = (·) and id_{Φ,x:A} = (id_{Φ}, x). The subscript Φ is dropped when

Variables  x, y, z
Meta variables  u, v, w
Sorts  s ::= type | kind
Atomic types  P, Q ::= a M
Types  A, B, C, D ::= P | Πx:A.B | Σx:A.B
Kinds  κ ::= type | Πx:A.κ
(Rigid) heads  H ::= a | c | x
Projections  π ::= fst | snd
Evaluation contexts  E ::= • | E N | π E
Neutral terms  R ::= E[H] | E[u[σ]]
Normal terms  M, N ::= R | λx.M | (M , N)
Substitutions  σ, τ ::= · | σ, M
Variable substitutions  ρ, ξ ::= · | ρ, x
Contexts  Ψ, Φ, Γ ::= · | Ψ, x:A
Signature  Σ ::= · | Σ, a:κ | Σ, c:A
Meta substitutions  θ, η ::= · | θ, Ψ̂.M/u
Meta contexts  Δ ::= · | Δ, u:A[Ψ]

Fig. 1. λ^{ΠΣ} with meta-variables

unambiguous. If Φ is a sub-context of Ψ (in particular if Ψ = Φ) then id_{Φ} is a well-formed substitution in Ψ, i.e., Ψ ⊢ id_{Φ} : Φ holds (see Fig. 2). We write Φ̂ for the list of variables dom(Φ) in order of declaration.

We write E[M] for plugging term M into the hole • of evaluation context E. This will be useful when describing the unification algorithm, since we often need to have access to the head of a neutral term. In the λ^{Π}-calculus, this is often achieved using the spine notation [1] simply writing H M_{1} … M_{n}. Evaluation contexts are the proper generalization of spines to projections.

Occurrences and free variables. If α, β are a syntactic entities such as evaluation context, term, or substitution, α, β ::= E | R | M | σ, we write α{β} if β is a part of α. If we subsequently write α{β′} then we mean the replacement of the indicated occurrence of β by β′. We say an occurrence is rigid if it is not part of a delayed substitution σ of a meta-variable, otherwise it is termed flexible. For instance, in c (u[y_{1}]) (x_{1} x_{2}) (λz. z x_{3} v[y_{2}, w[y_{3}]]) there are rigid occurrences of x_{1..3} and flexible occurrences of y_{1..3}. The meta-variables u, v appear in a rigid and w in a flexible position. A rigid occurrence is strong if it is not in the evaluation context of a free variable. In our example, only x_{2} does not occur strongly rigidly. Following Reed [16] we indicate rigid occurrences by α{β}^{rig} and strongly rigid occurrences by α{β}^{srig}.

We denote the set of free variables of α by FV(α) and the set of free meta variables by FMV(α). A superscript ^{rig} indicates to count only the rigidly occurring variables.

Typing rules are given in Figure 2. We have record types Σx:A. B but no record kinds Σx:A. κ. Our typing rules ensure that terms are in β-normal form, but

Neutral Terms/Types Δ; Ψ ⊢ R ⇒ A
{Σ(a) = κ \atop Δ; Ψ ⊢ a ⇒ κ} {Σ(c) = A \atop Δ; Ψ ⊢ c ⇒ A} {Ψ(x) = A \atop Δ; Ψ ⊢ x ⇒ A} \begin{matrix}u:A[Φ] ∈ Δ & Δ; Ψ ⊢ σ ⇐ Φ \\ Δ; Ψ ⊢ u[σ] ⇒ [σ]_{Φ}A \end{matrix}

\begin{matrix}Δ; Ψ ⊢ R ⇒ Πx:A.B & Δ; Ψ ⊢ M ⇐ A \\ Δ; Ψ ⊢ R M ⇒ [M/x]_{A}B \end{matrix}

{Δ; Ψ ⊢ R ⇒ Σx:A.B \atop Δ; Ψ ⊢ fst R ⇒ A} {Δ; Ψ ⊢ R ⇒ Σx:A.B \atop Δ; Ψ ⊢ snd R ⇒ [fst R/x]_{A}B}
Normal Terms Δ; Ψ ⊢ M ⇐ A

\begin{matrix}Δ; Ψ ⊢ R ⇒ A & A =_{η} C \\ Δ; Ψ ⊢ R ⇐ C \end{matrix}

{Δ; Ψ, x:A ⊢ M ⇐ B \atop Δ; Ψ ⊢ λx.M ⇐ Πx:A.B} \begin{matrix}Δ; Ψ ⊢ M ⇐ A & Δ; Ψ ⊢ N ⇐ [M/x]_{A}B \\ Δ; Ψ ⊢ (M , N) ⇐ Σx:A.B \end{matrix}
Substitutions Δ; Ψ ⊢ σ ⇐ Ψ′
Δ; Ψ ⊢ · ⇐ · \begin{matrix}Δ; Ψ ⊢ σ ⇐ Ψ′ & Δ; Ψ ⊢ M ⇐ [σ]_{Ψ′}A \\ Δ; Ψ ⊢ σ, M ⇐ Ψ′, x:A \end{matrix}
LF Types and Kinds Δ; Ψ ⊢ A ⇐ s
Δ; Ψ ⊢ P ⇒ type
Δ; Ψ ⊢ P ⇐ type

Δ; Ψ ⊢ A ⇐ type Δ; Ψ, x:A ⊢ B ⇐ type
Δ; Ψ ⊢ Σx:A.B ⇐ type
Δ; Ψ ⊢ type ⇐ kind  \begin{matrix}Δ; Ψ ⊢ A ⇐ type & Δ; Ψ, x:A ⊢ B ⇐ s \\ Δ; Ψ ⊢ Πx:A.B ⇐ s \end{matrix}
Meta-Substitutions Δ ⊢ θ ⇐ Δ′

for all u:A[Φ] ∈ Δ′ and Φ̂.M/u ∈ θ Δ; [[θ]]Φ ⊢ M ⇐ [[θ]]A

Δ ⊢ θ ⇐ Δ′
Meta-Context ⊢ Δ mctx

for all u:A[Ψ] ∈ Δ Δ ⊢ Ψ ctx Δ; Ψ ⊢ A ⇐ type

⊢ Δ mctx

Fig. 2. Typing rules for LF with meta-variables

they need not be η-long. The judgment A =_{η} C (rules omitted) compares A and C modulo η, i.e., modulo R = λx. R x (x ∉ FV(R)) and R = (fst R , snd R).

Hereditary substitution and meta-substitution. For α a well-typed entity in context Ψ and Δ; Φ ⊢ σ : Ψ a well-formed substitution, we facilitate a simultaneous substitution operation [σ]_{Ψ} (α) that substitutes the terms in σ for the variables as listed by Ψ in α and produces a β-normal result. Such an operation exists for well-typed terms, since λ^{ΠΣ} is normalizing. A naive implementation just substitutes and then normalizes, a refined implementation, called hereditary substitution [19], proceeds by resolving created redexes on the fly through new substitutions. Details can be found in Nanevski et al. [9], but do not concern us much here. Single substitution [N/x]_{A}(α) is conceived as a special case of simultaneous substitution. The type annotation A and the typing information in Ψ allow hereditary substitution to be defined by structural recursion; if no ambiguity arises, we may omit indices Ψ and A from substitutions.

The meta-substitution operation is written as [[Ψ̂.M/u]](N) and the simultaneous meta-substitution is written as [[θ]](N). When we apply Ψ̂.M/u to u[σ] we first substitute Ψ̂.M for u in the substitution σ to obtain σ′. Subsequently, we continue to apply σ′ to M hereditarily to obtain M′.

The typing rules ensure that the type of the instantiation Ψ̂.M and the type of u agree, i.e. we can replace u which has type A[Ψ] with a normal term M if M has type A in the context Ψ. Because of α-conversion, the variables that are substituted at different occurrences of u may be different, and we write Ψ̂.M where Ψ̂ binds all the free variables in M. We can always appropriately rename the bound variable in Ψ̂ such that they match the domain of the postponed substitution σ′. This complication can be eliminated in an implementation of the calculus based on de Bruijn indexes.

3 Constraint-based unification

We define the unification algorithm using rewrite rules which solve constraints incrementally. Constraints are defined as follows:

Constraint K ::= ⊤ | ⊥  trivial constraint and inconsistency
| Ψ ⊢ M = N : C unify term M with N
| Ψ | R:A ⊢ E = E′ unify evaluation context E with E′
| Ψ ⊢ u ← M : C  solution for u found
C. sets  K ::= K | K ∧ K  modulo laws of conjunction.

Our basic constraints are of the form Ψ ⊢ M = N : C. The type annotation Ψ ⊢ C serves two purposes: First, it is necessary to ensure that all substitutions created and used in our transformations can be properly annotated and hence we can use the fact that their application will terminate and produce again normal forms. Second, the type annotations in the context Ψ are necessary to eliminate Σ-types. For both purposes, simple types, i.e., the dependency-erasure of Ψ ⊢ C would suffice. However, we keep dependency in this presentation to scale this work from λ^{ΠΣ} to non-erasable dependent types such as in Agda.

A unification problem is described by Δ ⊩ K where Δ contains the typings of all the meta variables in K. A meta-variable u is solved, if there is a constraint Ψ ⊢ u ← M : C in K; otherwise we call u active. A solved metavariable does not appear in any other constraints nor in any type in Δ (nor in its solution M).

Intuitively, a set of constraints is well-formed if each constraint Ψ ⊢ M = N : C is well typed. Unfortunately, this is complicated by the fact that we may delay working on some sub-terms; to put it differently, we can work on subterms in an arbitrary order. Yet, the type of an equation may depend on the solvability of another postponed equation. Consider for example tuples. If (M_{1}, M_{2}) and (N_{1}, N_{2}) both have type Σx:A.B, then M_{1} and N_{1} have type A. However, types may get out of sync when we consider M_{2} and N_{2}. M_{2} has type [M_{1}/x]B while N_{2} has type [N_{1}/x]B, and we only know that their types agree, if we know that M_{1} is equal to N_{1}. Similar issues arise for function types and applications. Following Reed [16] we adopt here a weaker typing invariant, namely typing modulo constraints.

3.1 Typing modulo

For all typing judgments Δ; Ψ ⊢ J defined previously, we define Δ; Ψ ⊢_{K} J by the same rules as for Δ; Ψ ⊢ J except replacing syntactic equality = with =_{K}. We write Ψ̂.M =_{K} N if for any ground meta-substitution θ that is a ground solution for K, we have [[θ]]M = [[θ]]N. To put it differently, if we can solve K, we can establish that M is equal to N. Following Reed [16], substitution and meta-substitution preserve typing modulo.

Intuitively, a unification problem Δ ⊩ K is well-formed if all constraints (Ψ ⊢ M = N : C) ∈ K are well-typed modulo K, i.e., Δ; Ψ ⊢_{K} M ⇐ C and Δ; Ψ ⊢_{K} N ⇐ C. We will come back to this later when we prove correctness of our algorithm, but it is helpful to keep the typing invariant in mind when explaining the transitions in our algorithm.

3.2 A higher-order dynamic pattern unification algorithm for dependent types and records

The higher-order dynamic pattern unification algorithm is presented as rewrite rules on the set of constraints K in meta variable context Δ. The local simplification rules (Figure 3) apply to a single constraint, decomposing it and molding it towards a pattern by η-contraction and projection elimination. Decomposition of a neutral term is defined using evaluation contexts to have direct access to the head.

The other unification steps (Figure 4) work on a meta-variable and try to find an instantiation for it. Lowering rules transform a meta-variable of higher type to one of lower type. Flattening Σ-types concentrates on a meta-variable u:A[Φ] and eliminates Σ-types from the context Φ. The combination of the flattening Σtypes transition and the eliminating projections transition allow us to transform a unification problem into one which resembles our traditional pattern unification problem. The pruning transition is explained in detail in Section 3.4 and unifying a meta-variable with itself is discussed in Section 3.5.

Our algorithm can deal with a larger class of patterns where we require that meta-variables are associated with a linear substitution. To motivate our rules, let us consider some problems Ψ ⊢ u[σ] = M : C that fall out of the Miller pattern fragment, meaning that σ is not a list of disjoint variables. We may omit types and/or context if appropriate.

Decomposition of functions

Ψ ⊢ λx.M = λx.N : Πx:A. B  ↦_{d} Ψ, x:A ⊢ M = N : B
Ψ ⊢ λx.M = R : Πx:A. B  ↦_{d} Ψ, x:A ⊢ M = R x : B
Ψ ⊢ R = λx.M : Πx:A. B  ↦_{d} Ψ, x:A ⊢ R x = M : B

Decomposition of pairs

Ψ ⊢ (M_{1} , M_{2}) = (N_{1} , N_{2}) : Σx:A. B ↦_{d} Ψ ⊢ M_{1} = N_{1} : A ∧ Ψ ⊢ M_{2} = N_{2} : [M_{1}/x]B
Ψ ⊢ (M_{1} , M_{2}) = R : Σx:A. B  ↦_{d} Ψ ⊢ M_{1} = fst R : A ∧ Ψ ⊢ M_{2} = snd R : [M_{1}/x]B
Ψ ⊢ R = (M_{1} , M_{2}) : Σx:A. B  ↦_{d} Ψ ⊢ fst R = M_{1} : A ∧ Ψ ⊢ snd R = M_{2} : [fst R/x]B

Decomposition of neutrals

Ψ ⊢ E[H] = E′[H] : C  ↦_{d} Ψ | H : A ⊢ E = E′ where Ψ ⊢ H ⇒ A
Ψ ⊢ E[H] = E′[H′] : C  ↦_{d} ⊥ if H ≠ H′

Decomposition of evaluation contexts

Ψ | R : A ⊢ • = •  ↦_{d} ⊤
Ψ | R : Πx:A. B ⊢ E[• M] = E′[• M′] ↦_{d} Ψ ⊢ M = M′ : A ∧ Ψ | R M : [M/x]B ⊢ E = E′
Ψ | R : Σx:A. B ⊢ E[fst •] = E′[fst •] ↦_{d} Ψ | fst R : A ⊢ E = E′
Ψ | R : Σx:A. B ⊢ E[snd •] = E′[snd •] ↦_{d} Ψ | snd R : [fst R/x]B ⊢ E = E′
Ψ | R : Σx:A. B ⊢ E[π •] = E′[π′ •]  ↦_{d} ⊥ if π ≠ π′

Orientation

Ψ ⊢ M = u[σ] : C with M ≠ v[τ]  ↦_{d} Ψ ⊢ u[σ] = M : C

η-Contraction

Ψ ⊢ u[σ{λx. R x}] = N : C  ↦_{e} Ψ ⊢ u[σ{R}] = N : C
Ψ ⊢ u[σ{(fst R, snd R)}] = N : C  ↦_{e} Ψ ⊢ u[σ{R}] = N : C

Eliminating projections

Ψ_{1}, x : Πy:A. Σz:B.C, Ψ_{2}  Ψ_{1}, x_{1} : Πy:A. B, x_{2} : Πy:A. [(x_{1} y)/z]C, Ψ_{2}
⊢ u[σ{π (x M)}] = N : D ↦_{p} ⊢ u[[τ]σ] = [τ]N : [τ]D
where π ∈ {fst, snd}  where τ = [λy. (x_{1} y, x_{2} y)/x]

Fig. 3. Local simplification.

η-contraction u[λx. y (fst x , snd x)] = M Solved by contracting the l.h.s. to u[y].

Eliminating projections y : Πx:A. Σz:B. C ⊢ u[λx. fst (y x)] = M Applying substitution τ = [λx. (y_{1} x , y_{2} x)/y] yields problem y_{1} : Πx:A. B, y_{2} : Πx:A. [y_{1} x/z]C ⊢ u[λx. y_{1} x] = [τ]M which is solved by η-contraction, provided y_{2} ∉ FV([τ]M).

Lowering u : (Σx:A. B)[Φ] ⊩ fst (u[y]) = fst y This equation determines only the first component of the tuple u. Thus, decomposition into u[y] = y, which also determines the second component,

Local simplification

Δ ⊩ K ∧ K ↦ Δ ⊩ K ∧ K′  if K ↦_{m} K′  (m ∈ {d, e, p})

Instantiation (notation)

Δ ⊩ K + (Φ ⊢ u ← M : A)  = [[θ]]Δ ⊩ [[θ]]K ∧ [[θ]]Φ ⊢ u ← M : [[θ]]A
where θ = Φ̂.M/u

Lowering

Δ ⊩ K  ↦ Δ, v:B[Φ, x:A] ⊩ K
u:(Πx:A.B)[Φ] ∈ Δ active  + Φ ⊢ u ← λx.v : Πx:A. B
Δ ⊩ K  ↦ Δ, u_{1}:A[Φ], u_{2}:([u_{1}/x]_{A}B)[Φ] ⊩ K
u:(Σx:A.B)[Φ] ∈ Δ active  + Φ ⊢ u ← (u_{1} , u_{2}) : Σx:A. B

Flattening Σ-types

Δ ⊩ K (u:A[Φ] ∈ Δ active)  ↦ Δ, v:([σ^{−1}]A)[Φ′] ⊩ K + Φ ⊢ u ← v[σ] : A
Φ = Φ_{1}, x : Πy:A. Σz:B. C, Φ_{2}  Φ′ = Φ_{1}, x_{1} : Πy:A. B, x_{2} : Πy:A. [x_{1} y/z]C, Φ_{2}
σ^{−1} = [λy. (x_{1} y , x_{2} y)/x]  σ = [λy. fst (x y)/x_{1}, λy. snd (x y)/x_{2}]

Pruning

Δ ⊩ K  ↦ Δ′ ⊩ [[η]]K
(Ψ ⊢ u[ρ] = M : C) ∈ K  if Δ ⊢ prune_{ρ} M ⇒ Δ′; η and η ≠ id

Same meta-variable

Δ ⊩ K ∧ Ψ ⊢ u[ρ] = u[ξ] : C  ↦ Δ, v:A[Φ_{0}] ⊩ K + Φ ⊢ u ← v[id_{Φ_{0}}] : A
u:A[Φ] ∈ Δ  if ρ ∩ ξ : Φ ⇒ Φ_{0}

Failing occurs check

Δ ⊩ K ∧ Ψ ⊢ u[ρ] = M : C  ↦ ⊥ if FV^{rig}(M) ⊈ ρ
Δ ⊩ K ∧ Ψ ⊢ u[ρ] = M : C  ↦ ⊥ if M = M′{u[ξ]}^{srig} ≠ u[ξ]

Solving (with successful occurs check)

Δ ⊩ K ∧ Ψ ⊢ u[ρ] = M : C  ↦ Δ ⊩ K + Φ ⊢ u ← M′ : A
(u:A[Φ]) ∈ Δ; u ∉ FMV(M)  if M′ = [ρ/Φ̂]^{−1}M exists

Fig. 4. Unification steps.

loses solutions. Instead we replace u by a pair (u_{1}, u_{2}) of meta-variables of lower type, yielding u_{1} : A[Φ], u_{2} : ([u_{1}/x]B)[Φ] ⊩ u_{1}[y] = fst y.

Flattening Σ-types u : P [z : Πx:A. Σy:B. C] ⊩ u[λx. (z_{1} x , z_{2} x)] = M By splitting z into two functions z_{1}, z_{2} we arrive at u : P [z_{1} : Πx:A. B, z_{2} : Πx:A. [z_{1} x/y]C] ⊩ u[λx. z_{1} x, λx. z_{2} x] = M and continue with η-contraction.

Solving in spite of non-linearity u[x, x, z] = suc z The non-linear occurrence of x on the l.h.s. can be ignored since x is not free on the r.h.s. We can solve this constraint by by u[x, y, z] = suc z.

Pruning u[x] = suc(v[x, y]) and v[x, zero] = f(x, zero)

Since u depends only on x, necessarily v cannot depend on y. We can prune away the second parameter of v by setting v[x, y] = v′[x]. This turns the second constraint into the pattern v′[x] = f(x, zero), yielding the solution u[x] = suc(f(x, zero)). Note that pruning is more difficult in case of meta-variable nesting. If instead u[x] = suc(v[x, w[y]]) then there are two cases: either v does not depend on its second argument or w is constant. Pruning as we describe it in this article cannot be applied to this case; Reed [16] proceeds here by replacing y by a placeholder “ ”. Once w gets solved the placeholder might occur as argument to v, where it can be pruned. If the placeholder appears in a rigid position, the constraints have no solution.

Pruning and non-linearity u[x, x] = v[x] and u′[x, x] = v′[x, y] Even though we cannot solve for u due to the non-linear x, pruning x from v could lose solutions. However, we can prune y from v′ since only x can occur in v′[x, y].

Failing occurs check u[x] = suc y Pruning y fails because it occurs rigidly. The constraint set has no solution.

Same meta-variable u[x, y, x, z] = u[x, y, y, x] Since variables x, y, z are placeholders for arbitrary open well-typed terms, of which infinitely many exists for every type, the above equation can only hold if u does not depend on its 3rd and 4th argument. Thus, we can solve by u[x, y, z, x′] = v[x, y] where [x, y] is the intersection of the two variable environments [x, y, x, z] and [x, y, y, x].

Recursive occurrence u[x, y, x] = suc u[x, y, y] Here, u has a strong rigid occurrence in its own definition. Even though not in the pattern fragment, this only has an infinite solution: consider the instance u[z, z, z] = suc u[z, z, z]. Consequently, the occurs check signals unsolvability. [17, p. 105f] motivates why only strong rigid recursive occurrences force unsolvability. For instance, f : nat → nat ⊢ u[f] = suc (f (u[λx. zero])) has solution u[f] = suc (f (suc zero)) in spite of a rigid occurrence of u in its definition. If u occurs flexibly in its own definition, like in u[x] = v[u[x]], we cannot proceed until we know more of v. Using the other constraints, we might manage to prune v’s argument, arriving at u[x] = v[], or find the solution of v directly; in these cases, we can revisit the constraint on u.

The examples suggest a strategy for implementation: Lowering can be integrated triggered by decomposition to resolve eliminations of a meta variable E[u[σ]]. After decomposition we have a set of u[σ] = M problems. We try to turn the σs into variable substitutions by applying η-contraction, and where this gets stuck, elimination of projections and Σ-flattening. Solution of constraints u[ρ] = M can then be attempted by pruning, where a failing occurs check signals unsolvability.

3.3 Inverting substitutions

A most general solution for a constraint u[σ] = M can only be hoped for if σ is a variable substitution. For instance u[true] = true admits already two different solutions u[x] = x and u[x] = true that are pure λ-terms. In a language with computation such as Agda infinitely more solutions are possible, because u[x] could be defined by cases on x and the value of u[false] is completely undetermined.

But even constraints u[ρ] = M can be ambiguous if the variable substitution ρ is not linear, i. e., no bijective variable renaming. For example, u[x, x] = x has solutions u[x, y] = x and u[x, y] = y. Other examples, like u[x, x, z] = z, which has unique solution u[x, y, z] = z, suggest that we can ignore non-linear variable occurrences as long as they do not occur on the r.h.s. Indeed, if we define a variable substitution ρ to be invertible for term M if there is exactly one M′ such that [ρ]M′ = M, then linearity is a sufficient, but not necessary condition. However, it is necessary that ρ must be linear if restricted to the free variables of (β-normal!) M. Yet instead of computing the free variables of M, checking that ρ is invertible, inverting ρ and applying the result to M, we can directly try to invert the effect of the substitution ρ on M.

For a variable substitution Ψ ⊢ ρ ⇐ Φ and a term/substitution α ::= M | R | τ in context Ψ, we define the partial operation [ρ/Φ̂]^{−1}α by

[ρ/Φ̂]^{−1}x  = y  if x/y ∈ ρ/Φ̂ and there is no z ≠ y with x/z ∈ ρ/Φ̂,

undefined otherwise

[ρ/Φ̂]^{−1}c  = c
[ρ/Φ̂]^{−1}(u[τ]) = u[τ′] where τ′ = [ρ/Φ̂]^{−1}τ

and homeomorphic in all other cases.

We can show by induction on α, that inverse substitution [ρ/Φ̂]^{−1}α is correct, preserves well-typedness and commutes with meta substitutions.

3.4 Pruning

If the constraint u[σ] = M has a solution θ, then [[[θ]]σ]θ(u) = [[θ]]M, and since θ is closed (FMV(θ) = ∅), we have FV(σ) ⊇ FV([[θ]]M). Thus, if FV(M) ⊈ FV(σ) we can try to find a most general meta-substitution η which prunes the free variables of M that are not in the range of σ, such that FV([[η]]M) ⊆ FV(σ). For instance, in case u[x] = suc v[x, y], the meta-substitution x, y. v′[x]/v does the job. However, pruning fails either if pruned variables occur rigidly, like in u[x] = c y v[x, y] (constraint unsolvable), or if the flexible occurrence is under another meta variable, like in u[x] = v[x, w[x, y]]. Here, two minimal pruning substitutions η_{1} = x, y. v′[x]/v and η_{2} = x, y. w′[x]/w exist which are not instances of each other—applying pruning might lose solutions.

We restrict pruning to situations u[ρ] = M where ρ is a variable substitution. This is because we view pruning as a preparatory step to inverting ρ on M— which only makes sense for variable substitutions. Also, we do not consider partial pruning, as in pruning y from v in the situation u[x] = v[x, y, w[x, y]], obtaining u[x] = v′[x, w[x, y]]. Such extensions to pruning are thinkable, but we have no data indicating that they strengthen unification significantly in practice. Fig. 5 presents the rules for the judgements

prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} prune τ such that FV^{rig}([τ]id_{Ψ_{2}}) ⊆ ρ
Δ ⊢ prune_{ρ} M ⇒ Δ′; η prune M such that FV([[η]]M) ⊆ ρ.

prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} Prune τ : Ψ_{1}, returning a sub-context Ψ_{2} of Ψ_{1}.

prune ctx_{ρ}(· / ·) ⇒ ·

prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} FV^{rig}(M) ⊈ ρ
prune ctx_{ρ}(τ, M / Ψ_{1}, x:A) ⇒ Ψ_{2}
prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} FV(M) ⊆ ρ FV(A) ⊆ Ψ̂_{2}
prune ctx_{ρ}(τ, M / Ψ_{1}, x:A) ⇒ Ψ_{2}, x:A

Δ ⊢ prune_{ρ} M ⇒ Δ′; η Prune M, returning Δ′ ⊢ η ⇐ Δ.

v:B[Ψ_{1}] ∈ Δ prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} Ψ_{2} ≠ Ψ_{1} FV(B) ⊆ Ψ̂_{2} η = Ψ̂_{1}.v′/v
Δ ⊢ prune_{ρ}(v[τ]) ⇒ [[η]](Δ, v′:B[Ψ_{2}]); η
v:B[Ψ_{1}] ∈ Δ prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{1}
Δ ⊢ prune_{ρ}(v[τ]) ⇒ Δ; id_{Δ}

x ∈ ρ Δ ⊢ prune_{ρ} x ⇒ Δ; id_{Δ}

Δ ⊢ prune_{ρ} c ⇒ Δ; id_{Δ}

Δ ⊢ prune_{ρ} R ⇒ Δ_{1}; η_{1} Δ_{1} ⊢ prune_{ρ}([[η_{1}]]M) ⇒ Δ_{2}; η_{2}
Δ ⊢ prune_{ρ}(R M) ⇒ Δ_{2}; [[η_{2}]]η_{1}
Δ ⊢ prune_{ρ} M ⇒ Δ′; η
Δ ⊢ prune_{ρ}(π M) ⇒ Δ′; η

Δ ⊢ prune_{ρ,x} M ⇒ Δ′; η
Δ ⊢ prune_{ρ}(λx. M) ⇒ Δ′; η
Δ ⊢ prune_{ρ} M ⇒ Δ_{1}; η_{1} Δ_{1} ⊢ prune_{ρ}([[η_{1}]]N) ⇒ Δ_{2}; η_{2}
Δ ⊢ prune_{ρ} (M , N) ⇒ Δ_{2}; [[η_{2}]]η_{1}

Fig. 5. Pruning.

When pruning substitution τ with domain Ψ_{1} we look at each term M in τ which substitutes for an x:A of Ψ_{1}. If M has a rigid occurrence of a variable y ∉ ρ, we discard the entry x:A from the domain Ψ_{1}, thus, effectively removing M from τ. If M has no occurrence of such an y we keep x:A. However, since we might have removed prior entries from Ψ_{1} we need to ensure A is still well-formed, by validating that its free variables are bound in the pruned context. Finally, if M has a flexible occurrence of a y ∉ ρ, pruning fails. Examples:

1. prune ctx_{x}(c x, y / x′:A, y′:B) ⇒ x′:A
2. prune ctx_{y}(c x, y / x′:A, y′:B) ⇒ y′:B
3. prune ctx_{y}(c x, u[y] / x′:A, y′:B) ⇒ y′:B
4. prune ctx_{y}(u[x], y / x′:A, y′:B)  fails

Pruning a term M with respect to ρ ensures that all rigid variables of M are in the range of ρ (see variable rule). Also, for each rigid occurrence of a meta variable v[τ] in M we try to prune the substitution τ. If τ is already pruned, we leave v alone; otherwise, if the domain Ψ_{1} of τ shrinks to Ψ_{2} then we replace v : B[Ψ_{1}] by a new meta-variable v′ : B[Ψ_{2}] with domain Ψ_{2}. However, we need to ensure that the type B still makes sense in Ψ_{2}; otherwise, pruning fails.

Lemma 1 (Soundness and completeness of pruning).

1. If Δ ⊢_{K} Ψ_{1} ctx and prune ctx_{ρ}(τ / Ψ_{1}) ⇒ Ψ_{2} then Δ ⊢_{K} Ψ_{2} ctx and FV([τ]id_{Ψ_{2}}) ⊆ ρ. Additionally, if x ∈ Ψ_{1} \ Ψ_{2} then FV^{rig}([τ]x) ⊈ ρ.

2. If Δ ⊢ prune_{ρ} M ⇒ Δ′; η then Δ′ ⊢_{K} η ⇐ Δ and FV([[η]]M) ⊆ ρ. Also, if θ solves Ψ ⊢ u[ρ] = M_{0}{M}^{rig} : C then there is some θ′ such that θ = [[θ′]]η.

In an implementation, we may combine pruning with inverse substitution and the occurs check. Since we already traverse the term M for pruning, we may also check whether [ρ/Φ̂]^{−1}M exists and whether u occurs in M.

3.5 Unifying two identical existential variables

Any solution Φ̂.N/u for a meta variable u : A[Φ] with constraint u[ρ] = u[ξ] must fulfill [ρ]N = [ξ]N, which means that [ρ]x = [ξ]x for all x ∈ FV(N). This means that u can only depend on those of its variables in Φ that are mapped to the same term by ρ and ξ. Thus, we can substitute u by Φ̂.v[ρ′] where ρ′ is the intersection of substitutions ρ and ξ. Similarly to context pruning, we obtain ρ′ as [ρ]id_{Φ′}, which identical to [ξ]id_{Φ′}, where Φ′ is a subcontext of Φ mentioning only the variables that have a common image under ρ and ξ. This process is given as judgement ρ ∩ ξ : Φ ⇒ Φ′ with the following rules:

\begin{matrix}· ∩ · : · ⇒ · \\ {ρ ∩ ξ : Φ ⇒ Φ′ \atop (ρ, y) ∩ (ξ, y) : (Φ, x:A) ⇒ (Φ′, x:A)} & \begin{matrix}ρ ∩ ξ : Φ ⇒ Φ′ & z ≠ y \\ (ρ, z) ∩ (ξ, y) : (Φ, x:A) ⇒ Φ′ \end{matrix} \end{matrix}

Lemma 2 (Soundness of intersection). If Δ; Ψ ⊢_{K} ρ, ξ ⇐ Φ and ρ ∩ ξ : Φ ⇒ Φ′, then Δ ⊢_{K} Φ′ ctx and Δ; Φ ⊢_{K} id_{Φ′} ⇐ Φ′ and [ρ]id_{Φ′} = [ξ]id_{Φ′}.

Although we have restricted intersection to variable substitutions, it could be extended to meta-ground substitutions, i.e., substitutions that do not contain any meta-variables.

4 Correctness

Theorem 1 (Termination). The algorithm terminates and results in one of the following states:

– A solved sate where only assignments Ψ ⊢ u ← M : A remain.

– A stuck state, i.e., no transition rule applies.

– Failure ⊥.

Proof. The size |M| of a term be as usual the number of nodes and leaves in its tree representation, with the exception that we count λ-nodes twice. This modification has the effect that |λxM|+|R| > |M|+|R x|, hence, an η-expanding decomposition step also decreases the sum of the sizes of the involved terms [6].

We define the size |A[Φ]| of a type A in context Φ by |P [Φ]| = 1 + ∑_{A∈Φ} |A[]|, |(Πx:A. B)[Φ]| = 1 + |B[Φ, x:A]| and |(Σx:A. B)[Φ]| = 1 + |A[Φ]| + |B[Φ]|. The size of a type can then be obtained as |A| = |A[]| and the size of a context as |Φ| = ∑_{A∈Φ} |A|. The purpose of this measure is to give Σ-types a large weight that can “pay” for flattening.

The weight of a solved constraint be 0, whereas the weight |K| for a constraint Ψ ⊢ M = M′ : C be the ordinal (|M|+|M′|)ω+|Ψ| if a decomposition step can be applied, and simply |Ψ| else. Similarly, the weight of constraint Φ | R:A ⊢ E = E′ be (|E| + |E′|)ω + |Ψ|. Finally, the weight |Δ ⊩ K| of a unification problem be the ordinal

∑_{u:A[Φ]∈Δ active} |A[Φ]|ω^{2} + ∑_{K∈K} |K|.

By inspection of the transition rules we can show that each unification step reduces the weight of the unification problem. ⊓ ⊔

4.1 Solutions to unification

A solution to a set of equations K is a meta-substitution θ for all the metavariables in Δ s.t. Δ′ ⊢ θ ⇐ Δ and

1. for every Ψ ⊢ u ← M : A in K we have Ψ̂.M/u ∈ θ,

2. for all equations Ψ ⊢ M = N : A in K, we have [[θ]]M = [[θ]]N.

A ground solution to a set of equations K can be obtained from a solution to K by applying a grounding meta-substitution θ′ where · ⊢ θ′ ⇐ Δ′ to the solution θ. We write θ ∈ Sol(Δ ⊩ K) for a ground solution to the constraints K.

Next, we prove that transitions preserve solutions. We first observe that if we start in a state Δ_{0} ⊩ K_{0} and transition to a state Δ_{1} ⊩ K_{1} the meta-variable context strictly grows, i.e., dom(Δ_{0}) ⊆ dom(Δ_{1}). We subsequently show that if we have a solution for Δ_{0} ⊩ K_{0}, then transitioning to a new state Δ_{1} ⊩ K_{1} will not add any additional solutions nor will it destroy some solution we may already have. In other words, any additional constraints which may be added in Δ_{1} ⊩ K_{1} are consistent with the already existing solution.

Theorem 2 (Transitions preserve solutions). Let Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1}.

1. If θ_{0} ∈ Sol(Δ_{0} ⊩ K_{0}) then there exists a meta-substitution θ′ s.t. Δ_{1} ⊢ θ′ ⇐ Δ_{0} and a solution θ_{1} ∈ Sol(Δ_{1} ⊩ K_{1}) such that [[θ_{1}]]θ′ = θ_{0}.

2. If θ_{1} ∈ Sol(Δ_{1} ⊩ K_{1}) then [[θ_{1}]]id_{Δ_{0}} ∈ Sol(Δ_{0} ⊩ K_{0}).

4.2 Transitions preserve types

Our goal is to prove that if we start with a well-typed unification problem our transitions preserve the type, i.e., we can never reach an ill-typed state and hence, we cannot generate a solution which may contain an ill-typed term. In the statement below it is again important to note that the meta-context strictly grows, i.e., Δ_{0} ⊆ Δ_{1}. Therefore if Ψ, M, and A are well-formed with respect to Δ_{0}, they will be well-formed with respect to Δ_{1}.

Lemma 3 (Transitions preserve typing). Let Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1}.

1. If A =_{K_{0}} B, then A =_{K_{1}} B.

2. If Δ_{0}; Ψ ⊢_{K_{0}} M ⇐ A then Δ_{1}; Ψ ⊢_{K_{1}} M ⇐ A.

3. If Δ_{0}; Ψ ⊢_{K_{0}} R ⇒ A then Δ_{1}; Ψ ⊢_{K_{1}} R ⇒ A′ and A =_{K_{1}} A′.

Next, we define when a set of equations which constitute a unification problem are well-formed using the judgment Δ_{0} ⊩_{K_{0}} K wf, which states that each equation Ψ ⊢ M = N : A must be well-typed modulo the equations in K_{0}, i.e., Δ_{0}; Ψ ⊢_{K_{0}} M ⇐ A and Δ_{0}; Ψ ⊢_{K_{0}} N ⇐ A . We simply write Δ_{0} ⊩ K wf to mean Δ_{0} ⊩_{K} K wf.

Lemma 4 (Equations remain well-formed under meta-substitutions). If Δ_{0} ⊩ K wf and Δ_{1} ⊢_{K} θ ⇐ Δ_{0} then Δ_{1} ⊩ [[θ]]K wf.

Lemma 5 (Well-formedness of equations is preserved by transitions). If Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1} and Δ_{0} ⊩_{K_{0}} K wf then Δ_{1} ⊢_{K_{1}} K wf.

Theorem 3 (Unification preserves types). If Δ_{0} ⊩ K_{0} wf and Δ_{0} ⊩ K_{0} ↦ Δ_{1} ⊩ K_{1} then Δ_{1} ⊩ K_{1} wf.

5 Conclusion

We have presented a constraint-based unification algorithm which solves higherorder patterns dynamically and showed its correctness. We have extended higher-order pattern unification to handle Σ-types; this has been an open problem so far. In practice, this is important in systems such as Agda where Σ-types are commonly used, but unification cannot handle Σ-types effectively. In systems such as Beluga, Twelf or Delphin, a limited form of Σ-types arises due to the world or context declaration. To be able to state that multiple assumptions are introduced at the same time, these systems employ Σ-types. In Beluga, we have implemented the flattening of Σ-types and it works well in type reconstruction.

We thank Jason Reed for his insightful work and his explanations given via email.

References

1. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Journal of Logic and Computation, 13(5):639–688, 2003.

2. Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 259–273, Bonn, Germany, September 1996. MIT Press.

3. Dominic Duggan. Unification with extended patterns. Theoretical Computer Science, 206(1-2):1–50, 1998.

4. Conal Elliott. Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University, 1990. Available as Technical Report CMU-CS-90-134.

5. Roland Fettig and Bernd Löchner. Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. In 7th International Conference on Rewriting Techniques and Applications (RTA’96), New Brunswick, NJ, USA, volume 1103 of Lecture Notes in Computer Science (LNCS), pages 347– 361. Springer, 1996.

6. Healfdene Goguen. Justifying algorithms for βη conversion. In Proc. of the 8th Int. Conf. on Foundations of Software Science and Computational Structures, FoSSaCS 2005, volume 3441 of Lect. Notes in Comput. Sci., pages 410–424. Springer, 2005.

7. W. D. Goldfarb. The undecidability of the second-order unification problem. Theor. Comput. Sci., 13:225–230, 1981.

8. Dale Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255–269, Paris, France, June 1991. MIT Press.

9. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1–49, 2008.

10. Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Dept of Comput. Sci. and Engrg., Chalmers, Göteborg, Sweden, September 2007.

11. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007. Technical Report 33D.

12. Frank Pfenning and Carsten Schürmann. System description: Twelf — a metalogical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence, pages 202–206. Springer, 1999.

13. Brigitte Pientka. Tabled higher-order logic programming. PhD thesis, Department of Computer Science, Carnegie Mellon University, 2003. CMU-CS-03-185.

14. Brigitte Pientka and Joshua Dunfield. Beluga: a framework for programming and reasoning with deductive systems (System Description). In 5th International Joint Conference on Automated Reasoning (IJCAR’10), Lecture Notes in Artificial Intelligence (LNAI), 2010.

15. Adam Poswolsky and Carsten Schürmann. System description: Delphin—a functional programming language for deductive systems. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’08), volume 228 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 135–141. Elsevier, 2009.

16. Jason Reed. Higher-order constraint simplification in dependent type theory. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’09), 2009.

17. Jason Reed. A Hybrid Logical Framework. PhD thesis, School of Computer Science, Carnegie Mellon University, 2009.

18. Anders Schack-Nielson and Carsten Schürmann. Pattern unification for the lambda calculus with linear and affine types. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’10), volume 34 of Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 101–116, July 2010.

19. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2003.