Refining Refinement Types

Ewen Denney^{∗}

LFCS, Department of Computer Science, University of Edinburgh Kings Buildings, Edinburgh EH9 3JZ, Scotland Fax : +44 131 667 7209

                        Email : ewd@dcs.ed.ac.uk

September 12, 1997

Abstract We develop a theory of program specification using the notion of refinement type. This provides a notion of structured specification, useful for verification and program development. We axiomatise the satisfaction of specifications by programs as a generalised typing relation and give rules for refining specifications. A per semantics based on Henkin models is given, for which the system is proven to be sound and complete.

Keywords : specification, refinement, verification, type theory, Henkin models

1 Introduction

We address the question of what is a suitable notion of specification for a programming language, where the properties of interest can be expressed using some given program logic. In particular, we restrict our attention to those which can be studied using typed lambda calculi, that is, typed functional programming languages.

A number of possibilities can be considered. One is to say that a specification is a type in some expressive type theory. This is the approach taken by [Luo91] for example. The problem is that this only works for an intuitionistic logic. Classical logics are more common for specification, and cannot easily be encoded in type theories. Also, programming languages generally have a simple type system of their own, and this must somehow be related to the specification type theory.

Another possibility is to say that a specification is just a proposition of the program logic with a distinguished free variable. This is the approach traditionally taken by the program refinement community.

[Mor94] describes a refinement calculus based on the use of first-order predicate logic.

However, this approach has a number of shortcomings, which we illustrate with an example below. The main point is that for compositional verification and program development is it better to put more structure on specifications.

In this paper, we suggest a third possibility, a combination of the program logic with the type theory of the programming language which we call refinement types. The notion of refinement type has been studied extensively in program analysis (under different names) and there are many different systems, depending on the area of interest. The general idea is to have two levels — an underlying level of program types, and a more expressive level of program properties, which are then treated like types. For us, this more expressive level will be the specifications. Hence we can exploit type-theoretic structure in our specifications, but do not need to do any encoding.

∗Supported by a postgraduate research studentship from the Engineering and Physical Sciences Research Council

We describe a verification calculus based on the simply-typed lambda calculus with products (λ^{×→}) and some ground types such as nat and bool. The satisfaction of specifications by programs is axiomatised as a generalised typing relation. We do this by viewing specifications as refinements of an underlying type, expressed using the program logic. We use classical predicate logic as program logic here. We axiomatise an ordering on the refinement types, to be viewed as an increase in information, or refinement of specifications.

If P is a proposition in the logic containing free variable x with refinement type ϕ, where ϕ is a refinement of τ, then the subset type (x : ϕ)P is a refinement of type τ. It is convenient to combine this with dependent functions and products at the level of refinement types, even though the underlying types are not dependent.

Refinement types are not the same as subtypes though. For example, nat might be a subtype of real say, but not a refinement type. Though we are careful to distinguish refinement types from subtypes, equality is ‘stratified’ at different refinement types as in subtyping systems.

Contexts consist of both variable assumptions x : ϕ, and propositions P. These are combined so as to make explicit the mutual dependencies in well-formedness. The dependency arises because we allow refinement types in terms, which in turn can appear in propositions.

We give a simple set-theoretic interpretation of the calculus. The main result of the paper is soundness and completeness with respect to this class of models.

In Section 2 we consider a simple example of specifying and verifying a program in order to motivate the features of our calculus. We then give the syntax and rules of the calculus in Section 3. In Section 4 we return to the div2 example. Section 5 gives the semantics and proofs of soundness and completeness. Finally, we make some conclusions in Section 6.

Related Work

A number of authors have advocated program analysis using annotated type systems. An example in the ‘non-standard type system as program logic’ paradigm is [NN88], a system for binding time analysis (and optimisation). Jensen [Jen91] performs strictness analysis using intersection types and primitive types to indicate termination. Burn [Bur92] considers a more general framework, with intersection and union types. Each of these systems axiomatises property deductions using refinements ϕ ⊑ ϕ′.

Pfenning, who introduced the term “refinement type”, used them to express properties of mini-ML programs [FP91]. He also extended LF [Pfe93] with (possibly intensional) properties such as “in normal form” (a property of derivations). He does not allow refinement types in abstractions though. Pfenning adds primitive properties and intersection, whereas we add primitive predicate symbols.

There have been various approaches by type theorists to combining logic and types. Feferman’s system of variable types [Fef85] extends λ^{×→} with subset types, though equality does not depend on the type. Refinement of properties can be defined in the logic, and is not explicitly axiomatised. Talcott used a similar form of refinement types (though the underlying theory is untyped), based on Feferman’s work, in order to express local information for use in transformations to introduce continuations. Since she lacks a typed equality though, local assumptions can not be discharged and conclusions take the form “t = t′ in the context C[]”.

Aspinall [Asp95] presents a dependent type theory, λ_{≤{}}, which is formally similar in that it has subtyping on dependent functions and products. His system is based on subtyping rather than refinement types however. Dependency in λ_{≤{}} comes from singleton types, which are a special case of subset types.

Hayashi’s ATTT [Hay94b] is a rich type theory conservatively extending the polymorphic lambda calculus with singleton, union and intersection types. It is based on the refinement type philosophy, maintaining a distinction between types and specified subsets in order to eliminate non-computational information during program extraction. Refinement types are not allowed on abstractions. Dependent function and product types can be defined from the nondependent constructors [Hay94a], as well as subset types constructed using full second order intuitionistic logic.

As pointed out by Hayashi, schemas in the Z specification language can be seen as refinement types. They comprise two parts — a typing declaration, and a logical predicate given as a collection of axioms.

The deliverables approach [BM92, McK92] is to consider a program paired with its proof of correctness. We are similarly motivated in wanting to structure specifications using program types, but differ in taking proof existence as more important than the proof itself — terms do not need a witness to satisfy a refinement type. Our calculus could be regarded as an internal language for deliverables.

The work of Luo [Luo91] presents an encoding of specifications and ‘specification morphisms’ (corresponding to our terms) in an expressive type theory. Our work provides a more direct analysis of the concept of specification. The existential form of Martin-Löf’s type theory with subset types in [NPS90] is similar.

The program refinement community has traditionally used unstructured specifications of the (x : τ)P form. For example, Morgan [Mor94] describes a refinement calculus based on the use of propositions of first order predicate logic.

2 Example

Let us consider specifying division by 2 on the naturals and verifying that a program satisfies the specification. We will take the simply-typed lambda calculus and classical first-order predicate logic as simple programming and specification languages respectively. We will use an applied λ^{×→} theory extended with a constant for iteration over the naturals, where natiter z f n computes the n-th iterate f^{n}(z). As a first approximation to specifications we use propositions with a distinguished free variable, which we write as (x : τ)P where τ is the type of the variable x in proposition P.

A program div2 which implements division on the naturals is

                          div2 = λn : nat.π_{1}(div2′ n) : nat → nat

where this uses the auxiliary function

div2′ = natiter ⟨0, 0⟩ (λp : nat × nat.⟨π_{2}p, π_{1}p + 1⟩)

Now this can be specified as

div2 spec = (f : nat → nat) ∀n : nat.n = 2 ∗ fn ∨ n = 2 ∗ fn + 1

We want to axiomatise a satisfaction relation sat between programs (closed terms) and specifications, so that we can prove

                                  div2 sat div2 spec

One simple way of doing this is to say that t sat (x : τ)P is just taken to be a notation for a typing and a proposition, with derived rule

\begin{matrix}t : τ & P [t/x] \\ t sat (x : τ)P \end{matrix}  (1)

so this example reduces to proving

∀n : nat.n = 2 ∗ div2(n) ∨ n = 2 ∗ div2(n) + 1

Now, our specification language is rather cumbersome as it stands, so let us introduce dependent sums and products as abbreviations

Σ_{x:(x:σ)P} (y : τ)Q for (z : σ × τ)P [π_{1}z/x] ∧ Q[π_{1}z/x, π_{2}z/y]
Π_{x:(x:σ)P} (y : τ)Q for (f : σ → τ)∀x : τ.P ⊃ Q[fx/y]

If we allow ourself the further abbreviation of viewing types as trivial specifications, so that for example, nat can stand for (x : nat)true, then we can write our specification more compactly as

div2 spec = Π_{n:nat}(m : nat)n = 2 ∗ m ∨ n = 2 ∗ m + 1

Now, using our abbreviations, the following rule is admissible from our definition of sat

n : nat ⊢ π_{1}(div2′ n) sat (m : nat)n = 2m ∨ n = 2m + 1
λn : nat.π_{1}(div2′ n) sat Π_{n:nat}(m : nat)n = 2m ∨ n = 2m + 1

where we understand n : nat ⊢ t sat ϕ to mean for all closed t′ : nat, t[t′/n] sat ϕ[t′/n]. In general then, we want to consider satisfaction in an arbitrary context. Note the similarity to a typing rule. In fact, not only are Σ and Π useful structuring devices for specifications, they are also useful for proofs, as specifications of programs often tend to be most naturally expressed and proved in a ‘shape’ similar to the program.

For example, the program div2 is an abstraction and the specification div2 spec is of the form Π_{x:ϕ}ψ. The rule directly reflects a natural proof that div2 satisfies div2 spec. Similarly, the auxiliary function div2′ has specification

div2′ spec = Π_{n:nat}Σ_{(m:nat)n=2m∨n=2m+1}(m′ : nat)m + m′ = n

The proof of this, in turn, involves showing that a pair satisfies a product specification, and an abstraction satisfies a functional specification (as above). We also have to use induction to show that an iteration satisfies some specification parameterised on the naturals. We consider this example more fully in Section 4.

We do not throw away the original rule (1) however, since not all specifications can be given in a structured form.

A significant benefit in writing specification in this more structured form is conceptual — it is preferable to structure specifications for then the task of comprehension need not be duplicated unnecessarily for specification and program. Also, separate checks of well-formedness (i.e. type-checking here) and correctness, will involve some duplication of effort, so it is better to combine types and correctness properties. Though we will not consider it here, in order to be the basis of a useful program development methodology, it helps for our specifications and proofs to reflect the structure of the programs.

There is one final aspect of specifications which we must consider — equality. The kind of specifications with which we are concerned here are those which specify the input-output characteristics of programs. We are only interested in programs up to extensional equality. The alternative, in a typetheoretic setting, is to use an intensional equality and distinguish programs on the basis of syntactic form. This would be unnatural here however, so we view specifications as coming equipped with a partial equivalence relation (per), which acts as an equality. A per is a symmetric and transitive relation on the set of terms at the type, or equivalently, an equivalence relation on a subset of terms at the type.

For example, the specification Π_{l:nonemptylist}(n : nat)Min(n, l) where the proposition Min(n, l) says that n is the minimum element in list l, is a refinement type over type list → nat. We want to regard functions f, f′ : list → nat as equal solutions of this specification if they give the same results for nonempty lists. Any program satisfying this specification must be defined on the empty list, but we are not interested in the value it takes there.

Moreover, it is a useful abbreviation in specifications themselves to write =_{Π_{x:(x:σ)P} (y:τ)Q} where

t =_{Π_{x:(x:σ)P} (y:τ)Q} t′ when ∀x, x′ : σ.(x =_{σ} x′) ∧ P [x] ∧ P [x′] ⊃ (tx =_{τ} t′x′) ∧ Q[tx] ∧ Q[t′x′]

Now, we would attain some conceptual simplicity if specifications were to subsume types, satisfaction to subsume typing, and equality at a specification to subsume the usual equality at a type (which is often left implicit). For example, we use (n : nat)true in place of nat, and Σ_{n:(n:nat)true}(b : bool)true for nat × bool. However, Π_{x:(x:σ)P} (y : τ)Q is no longer an abbreviation since it represents a different equality now.

We believe it is misleading to regard specifications as types though, and refer to the specifications of this idealised specification language as refinement types. Equality is given by a per over the underlying type.

A specification therefore, is a refinement type, and consists of • a type τ

• a per ϕ over τ

We take a program in this calculus to be

• an equivalence class of a per ϕ

The alternative would be to take a program as an element of the domain of a per, but this would be unnatural because we would then be distinguishing programs beyond extensional equality.

We use a notation for the equivalence classes of pers, by allowing refinement types on the variables in abstractions. For example, λn : even.n is a class in the per even → nat but not nat → nat, and λn : nat.n is a class in both even → nat and nat → nat. The equality t =_{ϕ} t′ says that t and t′ are the same equivalence class of per ϕ.

For refinement types ϕ and ϕ′ over the same underlying type, we want to consider refinements ϕ ⊑ ϕ′, to be though of semantically as per inclusion (i.e. x =_{ϕ′} y ⊃ x =_{ϕ} y). We use the square ⊑ symbol to indicate an information ordering — the refinement of specifications.

3 The Calculus

We now give the syntax of the system and describe its judgements. Some syntactic results are then given and we give an operational intuition for the language.

3.1 Syntax

The idea is that we construct a theory of refinement types on top of an underlying λ^{×→} theory and a first-order logic theory.

Definition 3.1 A signature consists of a finite collection of ground types γ, and n-ary constants k, each of which is assigned some sort τ_{1}, …, τ_{n} → τ; a collection of n-ary predicates F, which are also assigned a sequence of types τ_{1}, …, τ_{n}, indicated by F : pred τ_{1}, …, τ_{n}; and axioms, that is, well-formed propositions and refinement typings in context, Γ ⊢ P, Γ ⊢ t : ϕ.

Although we do not have arbitrary refinement types as primitive in a signature, we get much the same expressiveness using primitive predicate symbols. For example, with the primitive type nat, we could have predicate even : prednat, and overload even for the refinement type (n : nat)even(n); constants ∗ : nat × nat → nat and inverse : nat → nat, with axiom inverse : Π_{n:(n:nat)n≠0}(m : nat)n ∗ m = 1.

The raw terms of the language are given by

Refinement types  ϕ ::= 1 | γ | Σ_{x:ϕ}ψ | Π_{x:ϕ}ψ | (x : ϕ)P
Terms  t ::= x | k(t_{1}, …, t_{n}) | ∗ | ⟨t, t′⟩ | λx : ϕ.t | π_{i}(t) | tt′
Propositions  P ::= false | P ⊃ P′ | ∀x : ϕ.P | F (t_{1}, …, t_{n}) | t =_{ϕ} t′ | ϕ ⊑ ϕ′
Contexts  Γ ::= ⟨⟩ | Γ, x : ϕ | Γ, P

We do not distinguish types and refinement types as syntactic categories. Refinement types should be viewed as being refinements of underlying types, so for example, if ϕ is over σ, and ψ is over τ, then Σ_{x:ϕ}ψ is over σ × τ. Formally however, types are just refinement types with no logical information, that is, without any (x : ϕ)P. We use σ and τ as metavariables for types.

There is a unique (up to equality) term ∗ of unit type 1. The meaning of the other refinement types in terms of satisfaction is that ⟨t, t′⟩ satisfies Σ_{x:ϕ}ψ when t satisfies ϕ and t′ satisfies ψ[t/x]; term t satisfies Π_{x:ϕ}ψ when for every t′ satisfying ϕ, tt′ is well-formed and satisfies ψ[t′/x]; and t satisfies (x : ϕ)P when it satisfies ϕ and the proposition P [t/x] holds.

Terms have their usual meaning in the lambda calculus, except that an abstraction λx : ϕ.t should be thought of as a simple specification of terms λx : σ.t′ such that for all t′′ which satisfy ϕ, t′[t′′/x] satisfies t[t′′/x]. We will refer to terms in the underlying λ^{×→} as total terms. For example, λn : even.n specifies total terms of type nat → nat which are the identity on even arguments. The application (λx : ϕ.t)t′′ is only well-formed for arguments t′′ which satisfy ϕ so behaviour outwith ϕ is not constrained. Note that this means that although even → even is a refinement of the type nat → nat, the term λn : even.n does not itself have type nat → nat. Intuitively, we can say that a term t has refinement type ϕ if its behaviour ‘at ϕ’ is uniquely determined, that is, any two total terms which satisfy t are themselves equal at ϕ.

The propositions are typed first order predicate logic of equalities and refinements. We use classical typed first-order logic as an example of a simple expressive logic.

We sometimes abbreviate the assumption x : (x : ϕ)P as x : ϕ|P.

Remark 3.1 Our choice of first-order classical logic is only significant insofar as it is an example of what we might call an extensional logic. We make essential use of the fact that for all terms t, t′ and propositions P, if t is extensionally equal to t′ (which, in general, may coincide with the equality of the logic, if it has one, but otherwise can be defined as a logical relation), then P [t/x] holds if and only if P [t′/x] does. In other words, we require Leibniz and observational equality to coincide.

Intuitionistic logic would be fine too, but these choices can be contrasted with, say, the use of an intensional logic such as the modal μ-calculus, where terms are viewed as transition systems through their reduction sequences.

3.2 Judgements

The judgements of the calculus are

Γ ⊢ t : ϕ
Γ ⊢ P

where the propositions include

Γ ⊢ t =_{ϕ} t′
Γ ⊢ ϕ ⊑ ϕ′

All judgements are made in a context Γ of variable assumptions x : ϕ and propositions P. There are also mutually dependent well-formedness judgements

                                        ⊢ Γ wf

Γ ⊢ ϕ : Ref τ
Γ ⊢ P wf

We say that a term t is well-formed in context Γ when there exists a refinement type ϕ such that Γ ⊢ t : ϕ. Note that ϕ need not be unique, though the underlying type is unique. Sometimes we write Γ ⊢ t, t′ : ϕ for Γ ⊢ t : ϕ and Γ ⊢ t : ϕ′.

The well-formedness judgement for refinement types, Γ ⊢ ϕ : Ref τ, says that refinement type ϕ in context Γ is over the type τ. We abbreviate ϕ : Ref τ as ϕ wf when the type τ is not significant.

We use g as a metavariable for environments, that is, tuples of terms which satisfy the refinement types and propositions in the context. We will use the abbreviations g : Γ, g =_{Γ} g′ and t[g/Γ] to indicate simultaneous satisfaction, equality and substitution respectively.

We understand Γ ⊢ t : ϕ to mean for all well-typed substitutions of the variables in Γ with g and g′, if g =_{Γ} g′, then t[g/Γ] =_{ϕ[g/Γ]} t[g′/Γ]. Although the use of g rather than g′ in the equality seems to introduce an asymmetry, it can be shown in fact that ϕ[g/Γ] = ϕ[g′/Γ].

3.3 Rules of the Calculus

The rules of the calculus are listed in the appendix, in figures 1-8. Well-formedness and proof judgements are mutually recursive. Figures 1 and 2 give the well-formedness rules for contexts and refinement types respectively. The well-formedness rules for propositions in figure 3 require that for an equality t =_{ϕ} t′ to be well-formed, the terms t and t′ have the property ϕ. This means for example, that n =even n′ is not well-formed in the context n : nat, n′ : nat. Refinements are only well-formed when the refinement types are over the same type.

In figure 4 we give the refinement typing rules, which also serve as well-formedness rules for the terms. These generalise the usual typing rules of λ^{×→} in the obvious way, with the addition of an introduction rule for refinement types. The natural elimination rule, t : (x : ϕ)P ⇒ t : ϕ, can be derived. We also need the rule (EQ) to infer a property from an equality. Finally, there is a weakening rule (WEAKEN), like the subsumption rule of subtyping systems.

Note that it is possible for the body of an abstraction to not be well-formed, just using the refinement type of the lambda, but the whole term to be well-formed at a particular refinement type. For example, we have λn : nat.(λm : even.m)n : even → nat, although the body is not well-formed in the context

n : nat.

Figures 5 and 6 give equality rules for terms. The well-formedness hypothesis in the congruence rule (CONG-EQ) is important since with stratified equalities, we require equality at the appropriate property.

In combination with (EQ), the rule (ABS-ξ-EQ) lets us prove (as in [Asp95]), for example, that λn : nat.n : even → even even though nat → nat and even → even are incomparable (which is an obstacle for some subtyping systems).

Example 3.1

n : nat, even(n) ⊢ n : nat nat ⊑ (n : nat)even(n) ^{REFTYPE-R-REF} n : even ⊢ n : even n : even ⊢ n =even n ^{REFL-EQ}

                        λn : even.n =_{even→even} λn : nat.n

ABS-ξ-EQ

                             λn : nat.n : even → even

EQ-PROP

Using the symmetry rule (SYMM-EQ) we can deduce the symmetric forms of (APP-ξ-EQ) and (PROJ2-ξ-EQ), e.g. if t =_{Σ_{x:ϕ}ψ} t′ then π_{2}(t) =_{ψ[π_{1}(t′)]} π_{2}(t′).

We seem to need the non-standard hypotheses for the η-rules. The usual hypothesis for (λ-β-EQ) would be Γ ⊢ t : Π_{x:ϕ}ψ. However, the following example makes essential use of it.

Example 3.2

f : nat → nat, ∀x : nat.even(fx), n : nat ⊢ fn : nat f : nat → nat, ∀x : nat.even(fx), n : nat ⊢ even(fn)
                      f : nat → nat, ∀x : nat.even(fx), n : nat ⊢ fn : even
                    f : nat → nat, ∀x : nat.even(fx) ⊢ f =_{nat→even} λn : nat.fn
                       f : nat → nat, ∀x : nat.even(fx) ⊢ f : nat → even

The η-rules enable us to combine logical and typing assumptions.

Similarly, we use (π-η-EQ) in order to prove, for example, that

z : σ × τ, P [π_{1}z], Q[π_{2}z] ⊢ z : (x : σ)P × (y : τ)Q

Figure 7 lists the refinement rules. There are the obvious ‘structural’ refinement rules for units and products, with a contravariant rule for functions, and rules for refinements involving subset types. We regard refinement as a proposition because we use logical reasoning to prove refinements. The rules for the other propositions are given in figure 8. This is a natural deduction presentation of typed classical predicate logic of equalities and refinements. Assumptions in context can be used via (HYP) or (REFTYPE-ELIM). The (CONG) rule actually follows from (CONG-EQ).

In order that when Γ ⊢ P is derivable, we have well-formedness of P in Γ, the rules (false-ELIM) and (HYP) have explicit well-formedness hypotheses. This prevents us proving non well-formed equalities

from false.

3.4 Metatheory

We prove a few syntactic results about the calculus. Some of the following results will be needed in Section 5 for proving completeness with respect to the semantics. Other standard metatheoretic results (not listed here) can be deduced from completeness.

We have the expected downward closure of equality with respect to refinement, as follows.

Proposition 3.1 The following rule is admissible.

\begin{matrix}Γ ⊢ t =_{ϕ′} t & Γ ⊢ ϕ ⊑ ϕ′ \\ Γ ⊢ t =_{ϕ} t′ \end{matrix}

Proposition 3.2 If closed t has type σ, then there exists a total term t′ such that ⊢ t =_{σ} t′.

Proof: Terms can only fail to be total by containing an abstraction with a refinement type. Either the abstraction is applied or it is not. If it is, reduce it (equality at the type). If not, then λx : ϕ.t : σ → τ, and we must have ϕ ⊑ σ, so λx : ϕ.t =_{σ→τ} λx : σ.t.

Well-formedness is a combination of typing and proving properties. This is illustrated in the following proposition.

Proposition 3.3 Given raw term t in well-formed context Γ, the following are equivalent :

1. Typify(t) is well-typed in typing context Typify(Γ), where Typify replaces ϕ : Ref τ with τ.

2. There exists a ϕ such that Γ, false ⊢ t : ϕ.

3. There exists a type τ, such that for all Γ ⊢ ϕ : Ref τ, we can prove Γ, false ⊢ t : ϕ.

We say that t is well-structured.

We will see in Section 5 that ⟦Γ ⊢ t⟧ is only defined for well-structured terms.

Lemma 3.1 It is an easy proof to show that for well-formed properties Γ ⊢ ϕ, we have reflexivity of refinement Γ ⊢ ϕ ⊑ ϕ. Some other derived refinements (assuming well-formedness where appropriate) are

1. \begin{matrix}Γ, x : ϕ ⊢ P′ ⊃ P & Γ ⊢ ϕ ⊑ ϕ′ \\ Γ ⊢ (x : ϕ)P ⊑ (x : ϕ′)P′ \end{matrix}

2. Γ, P ⊢ (x : ϕ)P = ϕ

3. Γ ⊢ (x : ϕ)true = ϕ

4. Γ ⊢ Π_{x:(x:ϕ)P} (y : ψ)Q ⊑ (f : Π_{x:ϕ}ψ)∀x : ϕ.P ⊃ Q[fx/y]

5.

Γ ⊢ ϕ wf Γ, x : ϕ ⊢ ψ wf Γ, x : ϕ, y : ψ ⊢ Q wf

Γ ⊢ Π_{x:ϕ}(y : ψ)Q = (f : Π_{x:ϕ}ψ)∀x : ϕ.Q[fx/y]

6. Γ ⊢ Σ_{x:(x:ϕ)P} (y : ψ)Q = (z : Σ_{x:ϕ}ψ)P [π_{1}z/x] ∧ Q[π_{1}z/x, π_{2}z/y]

7. Γ ⊢ (x : (y : ϕ)P [y])Q[x] = (z : ϕ)P [z] ∧ Q[z] Proposition 3.4 If Γ ⊢ ϕ, ϕ′ : Ref τ, then Γ ⊢ ϕ ⊑ (x : ϕ′)false.

Remark 3.2 Refinement is a definitional extension of refinement typing in the sense that Γ, x : ϕ′ ⊢ x : ϕ whenever Γ ⊢ ϕ ⊑ ϕ′.

{Γ, x : ϕ′ ⊢ x : ϕ \atop Γ, x : ϕ′, true ⊢ x : ϕ} Γ ⊢ ϕ ⊑ (x : ϕ′)true ^{REFTYPE-R-REF} Γ ⊢ ϕ′ ⊑ ϕ′ Γ, x : ϕ′ ⊢ true Γ ⊢ (x : ϕ′)true ⊑ ϕ′ ^{REFTYPE-L-REF}
Γ ⊢ ϕ ⊑ ϕ′

However, this does not mean that the refinement rules are superfluous, and that proofs of refinement always reduce to typing. In practice, when working backwards from ϕ ⊑ ϕ′, we only make use of the refinement type rules, via REFTYPE-R-REF, when ϕ′ is of the form (x : ψ)Q.

The rules ABS-ξ-EQ and WEAKEN have refinements as hypotheses and they are needed to prove x : (x : ϕ)P ⊢ x : ϕ. Therefore, as the rules stand, we cannot treat ϕ ⊑ ϕ′ as syntactic sugar for Γ, x : ϕ′ ⊢ x : ϕ.

3.5 Operational intuition

The operational intuition behind equality and satisfaction of refinement types can be expressed in terms of a notion of (closed) total term. Recall that programs are to be thought of as equivalence classes of pers. We expect

t : ϕ when ∀u, u′ ∈ Total(t) . u ∼_{ϕ} u′
t =_{ϕ} t′ when ∀u ∈ Total(t).∀u′ ∈ Total(t′) . u ∼_{ϕ} u′

where we pick some definition of Total(t) and a notion of equivalence on total terms ∼_{ϕ}.

Definition 3.2 We define a logical relation ∼_{ϕ} between total terms, a function Total which takes a closed term to its set of total realizers, and relations ≃_{ϕ} between arbitrary terms. For example, Total(⟨λn : even.n, ∗⟩) is the set of pairs ⟨f, ∗⟩, such that total f is an identity on evens.

• – u_{1} ∼_{1} u_{2} when u_{1} =_{1} u_{2} – u_{1} ∼_{γ} u_{2} when u_{1} =_{γ} u_{2}

– u_{1} ∼_{Σ_{x:ϕ}ψ} u_{2} when π_{1}(u_{1}) ∼_{ϕ} π_{1}(u_{2}) and π_{2}(u_{1}) ∼_{ψ[π_{1}(u_{1})]} π_{2}(u_{2})

– u_{1} ∼_{Π_{x:ϕ}ψ} u_{2} when for all u′_{1} ∼_{ϕ} u′_{2}, u_{1}u′_{1} ∼_{ψ[u′_{1}]} u_{2}u′_{2}

– u_{1} ∼_{(x:ϕ)P} u_{2} when u_{1} ∼_{ϕ} u_{2} and P̃[u_{1}], P̃[u_{2}] where P̃ is P with each =_{ϕ} replaced by ≃_{ϕ}.

• – Total(k) = {k} – Total(∗) = {∗}

– Total(⟨t, t′⟩) = {⟨u, u′⟩ | u ∈ Total(t), u′ ∈ Total(t′)}

– Total(λx : ϕ.t) = {f : σ → τ | ∀u ∼_{ϕ} u.fu ∈ Total(t[u/x])}

– Total(π_{i}(t)) = {π_{i}(u) | u ∈ Total(t)}

– Total(tt′) = {uu′ | u ∈ Total(t), u′ ∈ Total(t′)}

• t ≃_{ϕ} t′ when for all u ∈ Total(t), u′ ∈ Total(t′), we have u ∼_{ϕ} u′

Note that ≃_{ϕ} is not the same as =_{ϕ}. For example,

                    λf : nat → nat.3 ≃_{(even→nat)→nat} λf : even → nat.3

This gives the basis of an operational semantics, although we do not pursue this here. We use it to characterise the term model in Section 5.

Proposition 3.5 ≃ is a congruence, that is, for x : ϕ ⊢ t′′ : ψ, if t ≃_{ϕ} t′ then t′′[t/x] ≃_{ψ[t/x]} t′′[t′/x].

4 Division by 2 revisited

As an illustration of how refinement types can provide a useful proof technique, we give the division by 2 example from the introduction again.

First, we give the inference rules for primitive and well-founded recursion over naturals, which combine the typing rules for recursion constants with the induction rules, into a single refinement typing. The sort is

                            natrec : τ, (nat → τ → τ), nat → τ

and the axiom schemas are (for each ϕ)

Γ ⊢ n : nat Γ ⊢ t : ϕ[0] Γ ⊢ t′ : Π_{n:nat}ϕ[n] → ϕ[succ n]
Γ ⊢ natrec t t′ n : ϕ[n]
Γ ⊢ t : ϕ[0] Γ ⊢ t′ : Π_{n:nat}ϕ[n] → ϕ[succ n]
Γ ⊢ natrec t t′ 0 =_{ϕ[0]} t
Γ ⊢ t : ϕ[0] Γ ⊢ t′ : Π_{n:nat}ϕ[n] → ϕ[succ n]

                         Γ ⊢ natrec t t′ succ n = t′ n (natrec t t′ n)

We define iteration from the more general recursion, as

                          natiter t t′ n = natrec t (λx : nat.t′) n

where x ∉ t′.

The program is

                               div2 = λn : nat.π_{1}(div2′ n)

div2′ = natiter ⟨0, 0⟩ (λp : nat × nat.⟨π_{2}p, π_{1}p + 1⟩)

We prove that it satisfies the specification

div2 : Π_{n:nat}(m : nat)n = 2m ∨ n = 2m + 1
div2′ : Π_{n:nat}Σ_{(m:nat)n=2m∨n=2m+1}(m′ : nat)m + m′ = n

In fact, there is little of interest in the main part of the proof. Since refinement types explicitly indicate the structure of the specification, this enables much of the proof to be carried out in a syntax-directed fashion. This would be useful for automation.

Write ϕ[n] as an abbreviation for Σ_{m:(m:nat)n=2m∨n=2m+1}(m′ : nat)m + m′ = n.

⟨0, 0⟩ : ϕ[0]

{see below \atop n : nat, p : ϕ[n] ⊢ ⟨π_{2}p, π_{1}p + 1⟩ : ϕ[n + 1]} n : nat ⊢ nat × nat ⊑ ϕ[n]
n : nat ⊢ λp : nat × nat.⟨π_{2}p, π_{1}p + 1⟩ : ϕ[n] → ϕ[n + 1]
n : nat ⊢ natiter ⟨0, 0⟩ (λp : nat × nat.⟨π_{2}p, π_{1}p + 1⟩) n :
Σ_{(m:nat)n=2m∨n=2m+1}(m′ : nat)m + m′ = n
λn : nat.natiter ⟨0, 0⟩ (λp : nat × nat.⟨π_{2}p, π_{1}p + 1⟩) n :
Π_{n:nat}Σ_{(m:nat)n=2m∨n=2m+1}(m′ : nat)m + m′ = n

The proof continues with

{n : nat, n = 2π_{1}p ∨ n = 2π_{1}p + 1 ⊢ n + 1 = 2π_{2}p ∨ n + 1 = 2π_{2}p + 1 \atop n : nat, p : ϕ[n] ⊢ n + 1 = 2π_{2}p ∨ n + 1 = 2π_{2}p + 1}

n : nat, p : ϕ[n] ⊢ π_{2}p : (m : nat)n + 1 = 2m ∨ n + 1 = 2m + 1

The remainder of the proof is arithmetic reasoning. In practice, we would use a theorem prover here.

{n : nat, p : ϕ[n] ⊢ π_{1}p + π_{2}p = n \atop n : nat, p : ϕ[n] ⊢ π_{2}p + π_{1}p + 1 = n + 1}

5 Models

We give interpretations of the calculus in Henkin models with per structure. As is usual in concrete models of applied lambda calculi, we must consider general Henkin models in order to get completeness. The per structure is to account for stratified equalities at different refinement types.

A Henkin model (with products) is an applicative structure

⟨{A^{σ}}, {Proj_{1}^{σ,τ} }, {Proj_{2}^{σ,τ} }, {App^{σ,τ} }, Const⟩

which is also extensional and satisfies the environment model condition. See [Mit96] for details. In addition, we require a function Pred which interprets predicates

Pred(F) ⊆ A^{τ_{1}×...×τ_{n}}, for F : pred τ_{1}, …, τ_{n}

It is extensionality which allows us to interpret abstractions, pairs and the unit uniquely, up to equality in the appropriate per, and the environment model condition which gives us enough elements. To each type σ we ascribe the set A^{σ}, and use Const to map constants into the appropriate sets. For each constant k : γ, we have Const(k) ∈ A^{γ}. The constant k : τ_{1}, …, τ_{n} → τ is mapped into the set A^{τ_{1}×...×τ_{n}→τ}. Note that we do not have A^{σ×τ} = A^{σ} ×A^{τ} in general, but have an isomorphism mediated by projection functions, Proj_{1}^{σ,τ} : A^{σ×τ} → A^{σ}, and Proj_{2}^{σ,τ} : A^{σ×τ} → A^{τ}. Similarly, A^{σ→τ} is not A^{σ} → A^{τ} in general, but may be embedded in it.

The idea is that refinement types over type σ are interpreted as pers over A^{σ}. Primitive types are interpreted as the identity per over their set. It is easy to see that, in fact, all types are interpreted as identities.

A Henkin model A models an applied theory when all constants and predicates are given an interpretation, and each axiom is true in the model.

However, terms, refinement types and propositions are all interpreted in context, so we must first define environments g for context Γ, written g ⊨ Γ, where g is a tuple of elements in the domains of the pers for the refinement types in Γ. We define this recursively with the interpretation of refinement types and propositions :

⟨⟩ ⊨ ⟨⟩
⟨g, a⟩ ⊨ Γ, x : ϕ when g ⊨ Γ and a ∈ ⟦Γ ⊢ ϕ⟧(g)
g ⊨ Γ, P when g ⊨ Γ and g ∈ ⟦Γ ⊢ P ⟧

For g, g′ ⊨ Γ we define g =_{Γ} g′ in the obvious way.

The interpretations are given in the appendix.

To avoid questions of coherence, we interpret raw terms^{1}, and so raw propositions and refinement types too. We define the interpretation of the refinement type in context Γ ⊢ ϕ, for each environment g ⊨ Γ, in figure 9. There is an apparent asymmetry in the definition of the product per for Σ_{x:ϕ}ψ, but this is not so, for if ϕ is a well-formed refinement type in context Γ, then if g⟦Γ⟧g′ we have ⟦Γ ⊢ ϕ⟧g = ⟦Γ ⊢ ϕ⟧g′.

The raw term in context Γ ⊢ t is interpreted in environment g ⊨ Γ as a subset (its ‘total realizers’) of A^{σ}. We interpret a raw proposition in context Γ ⊢ P as the set of environments g ⊨ Γ in which P holds.

We may now say what the semantic analogues of the judgements are. For per R, write a ∈ R to mean a R a. We often write the relation as =_{R}. Define Γ ⊨ t : ϕ when for all models A, for all g =_{⟦Γ⟧} g′, for all a ∈ ⟦Γ ⊢ t⟧(g) and a′ ∈ ⟦Γ ⊢ t′⟧(g′), we have a =_{⟦Γ⊢ϕ⟧(g)} a′. In other words, the interpretation is unique up to the equality of the per. We say that Γ ⊨ P when ⟦Γ ⊢ P ⟧ = {g | g ⊨ Γ}. In particular, the refinement Γ ⊨ ϕ ⊑ ϕ′ is valid when for all g ⊨ Γ, there is an inclusion of pers ⟦Γ ⊢ ϕ′⟧(g) ⊆ ⟦Γ ⊢ ϕ⟧(g).

1In fact, only well-structured terms are given an interpretation. For example, (λn : even.n)∗ does not have a well-defined interpretation, but (λn : even.n)3 does, even though it is not syntactically well-formed.

We define Γ ⊨ ϕ wf to mean for all g =_{⟦Γ⟧} g′, ⟦Γ ⊢ ϕ⟧(g) = ⟦Γ ⊢ ϕ⟧(g′). Also, Γ ⊨ P wf is convenient notation for, for all g =_{⟦Γ⟧} g′, g ∈ ⟦Γ ⊢ P ⟧ ⟺ g′ ∈ ⟦Γ ⊢ P ⟧.

First we give a substitution lemma. Since total terms are interpreted as singleton sets, we abuse notation and write ⟦u⟧ for both the set and its unique inhabitant.

Lemma 5.1 (Substitution Lemma) For total terms u, and appropriate well-formed contexts, g, g′,

1. ⟦Γ, x : ϕ, Γ′ ⊢ ψ⟧⟨g, ⟦u⟧, g′⟩ = ⟦Γ, Γ′[u] ⊢ ψ[u]⟧⟨g, g′⟩

2. ⟨g, ⟦u⟧, g′⟩ ∈ ⟦Γ, x : ϕ, Γ′ ⊢ P ⟧ ⟺ ⟨g, g′⟩⟦Γ, Γ′[u] ⊢ ψ[u]⟧⟨g, g′⟩

3. ⟦Γ, x : ϕ, Γ′ ⊢ t⟧⟨g, ⟦u⟧, g′⟩ = ⟦Γ, Γ′[u] ⊢ t[u]⟧⟨g, g′⟩

Proof: Induct simultaneously over open terms, refinement types and propositions.

Lemma 5.2 Suppose ⟦t⟧ =_{⟦ϕ⟧} ⟦t′⟧. Note that we do not require t, t′ : ϕ. Then,

1. If x : ϕ ⊨ ψ wf then ⟦ψ[t]⟧ = ⟦ψ[t′]⟧

2. If x : ϕ ⊨ P wf then ⊨ P [t] iff ⊨ P [t′]

3. If x : ϕ ⊨ t′′ : ψ then ⟦t′′[t]⟧ =_{⟦ψ[t]⟧} ⟦t′′[t′]⟧

Proof: Simultaneous induction over terms, refinement types and propositions.

Lemma 5.3 For ⊨ t : ϕ, and x : ϕ ⊨ P wf, if ⟦t⟧ ⊆ ⟦x : ϕ ⊢ P ⟧ then ⊨ P [t].

Proof: Let u ∈ Total(t), so u ≃_{ϕ} t. Then singleton ⟦u⟧ ⊆ ⟦t⟧. By soundness of t : ϕ, we have ⟦t⟧ =_{⟦ϕ⟧} ⟦u⟧, so since ⟦u⟧ ⊆ ⟦x : ϕ ⊢ P ⟧, by Lemma 5.1, ⊨ P [u]. Since ⟦t⟧ =_{⟦ϕ⟧} ⟦u⟧, Lemma 5.2 gives ⊨ P [t].

We have

Theorem 5.1 (Soundness) If Γ ⊢ t : ϕ then Γ ⊨ t : ϕ, if Γ ⊢ ϕ wf then Γ ⊨ ϕ wf, if Γ ⊢ P wf then Γ ⊨ P wf, and if Γ ⊢ P then Γ ⊨ P.

Proof: Simultaneous induction over all derivations.

The soundness of λ-β-EQ uses Lemma 5.3. Assume that Γ, x : ϕ ⊨ t : ψ, Γ ⊨ t′ : ϕ, and let g =_{⟦Γ⟧} g′, a ∈ ⟦Γ ⊢ (λx : ϕ.t)t′⟧(g), a′ ∈ ⟦Γ ⊢ t[t′/x]⟧(g′). Then a =_{⟦Γ⊢ψ[t′/x]⟧(g)} a′. The soundness of ∀-ELIM is similar.

We want to show that if a particular judgement holds in all the models (of the relevant signature) then it is provable. Although we do not have minimal models (due to having propositional assumptions), we can still use a term model construction, using a slight generalisation of the standard ‘consistency implies satisfiability’ argument.

First we generalise consistency and satisfiability from sets of closed propositions to arbitrary contexts. Say that context Γ is

• consistent, when Γ ⊬ false

• satisfiable, when there exists a model A and environment g in A such that g ⊨_{A} Γ

In the case that Γ is a context of closed propositions, these reduce to the usual definitions. Now we want to show that Γ ⊨ P ⇒ Γ ⊢ P, so suppose Γ ⊬ P. Then Γ, ¬P is consistent and so, by assumption, is satisfiable. Hence Γ ⊭ P. We must stipulate that the proposition is well-formed because it is possible that t =_{ϕ} t is true in the model, but t : ϕ is not provable.

We must be careful with the statement of completeness. This is because it is possible for non well-formed terms to have a unique interpretation, and so, semantically, have a refinement type. For example, (λn : even.∗)3 is interpreted as the unique inhabitant of unit type, but cannot be typed in the system. Also, λf : nat → nat.3 has the refinement type (even → nat) → nat in the model, but not in the calculus.

What we can show however, is that if a term t has refinement type ϕ in the model, then there exists a term t′ which does satisfy refinement type ϕ, such that t ≃_{ϕ} t′, and so ⊨ t =_{ϕ} t′. We write this as t ∼ ϕ.

Theorem 5.2 (Completeness) For Γ ⊢ P wf, if Γ ⊨ P then Γ ⊢ P. For Γ ⊢ ϕ wf, if Γ ⊨ t : ϕ then Γ ⊢ t ∼ ϕ.

Proof: Let Γ be a consistent context. We sketch the construction of a model A and environment g ⊨_{A} Γ below. We will just consider unary predicate symbols.

1. Let A = {P | Γ ⊢ P wf}. Construct a maximal consistent Henkin theory Δ such that {P | Γ ⊢ P } ⊆ Δ ⊆ A.

A Henkin^{2} theory T, is a collection of sentences closed under derivation, such that if the proposition ∃x : ϕ.P is in T, then P [t/x] is in T for some t : ϕ.

The construction of the Henkin theory involves adding constants c_{ϕ,P} : τ, and axioms c_{ϕ,P} : ϕ, P [c_{ϕ,P}], for each refinement type Γ ⊢ ϕ : Ref τ, and propositions Γ ⊢ P wf, for each ∃x : ϕ.P in T.

The existence of maximal consistent Henkin extensions follows using a standard argument from Zorn’s Lemma. See [vD94] for details. Note that for all Γ ⊢ P wf exactly one of P, ¬P is in Δ.

2. Let Γ_{∞} be a set of infinitely many declarations x : ϕ for each closed inhabited ϕ, i.e. for which there exists t such that ⊢ t : ϕ. This is so that we can construct a model from open terms.

3. Define a family of logical equivalence relations, R_{Δ}^{τ}( , ) for each type τ, on open terms of λ^{×→}with type τ, {t | Γ_{∞} ⊢ t : τ}, as R_{Δ}^{τ}(t, t′) ⟺ Δ_{∞} ⊢ t =_{τ} t′.

4. Define A^{τ} as the set of equivalence classes with respect to R of open terms in τ, and construct a Henkin model A, by interpreting constants syntactically. Interpret predicates F : pred τ as {[t] | F (t) ∈ Δ}.

5. Hence A models Δ, so it models Γ. The set Δ gives rise to an environment for Γ in A. Now for every x : ϕ ∈ Γ there is a proposition x =_{ϕ′} t ∈ Δ, where t is closed, and ϕ′ is a closed instantiation of ϕ. So Δ is effectively a set of closed propositions.

We use ĝ below for the tuple of elements t and g for the total elements u.

For x : ϕ ∈ Γ, define the corresponding element in the environment as g_{x} = [u]^{τ}, where x =_{ϕ′} t ∈ Δ and u is any total realizer of t (which does exist).

6. We abbreviate ⟦ ⟧(g) with ⟦ ⟧ and g ∈ ⟦Γ ⊢ P ⟧ by A ⊨ P.

For Γ ⊢ P wf, prove that A ⊨ P ⟺ Δ_{∞} ⊢ P ⟺ Δ ⊢ P. The second equivalence is because for each x : ϕ ∈ Γ_{∞}, x ∉ P and ϕ is inhabited.

In order to prove the first equivalence in step 5, we need a number of lemmas. First we characterise the interpretation of terms and refinement types in the term model, A. In the following, the semantic interpretation ⟦ ⟧ is to be understood as being in A. As pointed out in Section 3.5, the pers do not correspond exactly to equality.

Lemma 5.4

[u] ⟦Γ ⊢ ϕ⟧(g) [u′] ⟺ Δ_{∞} ⊢ u ∼_{ϕ[g/Γ]} u′

2Nothing to do with Henkin models.

Lemma 5.5 For closed raw terms t,

⟦t⟧ = Total(t), that is, {[u] | Δ_{∞} ⊢ u : σ, u ∈ Total(t)}

Hence t =_{ϕ} t′ in the term model is t ≃_{ϕ} t′.

Proof of Theorem 5.2 cont.:

We now prove that for all Γ ⊢ J wf, A ⊨ J ⟺ Δ_{∞} ⊢ J̃ by simultaneous induction over all judgements. By J̃ we mean replacing t : ϕ with t ∼ ϕ.

By well-formedness of t : ϕ we mean well-formedness of ϕ. Recall that this is all with respect to an environment g for context Γ.

The inductive ordering is

P, P′ < P ⊃ P′
ϕ, P [t] < ∀x : ϕ.P
ϕ < t =_{ϕ} t′
ϕ, ϕ′ < ϕ ⊑ ϕ′
ϕ, ψ[t] < Σ_{x:ϕ}ψ
ϕ, ψ[t] < Π_{x:ϕ}ψ
ϕ, ψ[t] < (x : ϕ)P

where the ϕ case means the truth or otherwise of t : ϕ for each t, i.e. for each t, ⊨ t : ϕ ⇒⊢ t ∼ ϕ.

• A ⊨ P ∧ Q ⟺ A ⊨ P and A ⊨ Q ⟺ Δ_{∞} ⊢ P and Δ_{∞} ⊢ Q ⟺ Δ_{∞} ⊢ P ∧ Q

• A ⊭ false, and Δ_{∞} ⊬ false since consistent

• A ⊨ ∀x : ϕP when for all a ∈ ⟦ϕ⟧, a ∈ ⟦x : ϕ ⊢ P ⟧. Now if Γ ⊢ t : ϕ, by soundness we have ⟨g, ⟦t⟧⟩ ⊆ ⟦Γ, x : ϕ ⊢ P ⟧, and so by Lemma 5.3, A ⊨ P [t], and by the inductive hypothesis, Δ_{∞} ⊢ P [t]. In other words, for all Γ ⊢ t : ϕ we have Δ_{∞} ⊢ P [t]. Thus Δ_{∞} ⊢ ∀x : ϕ.P [x], for if not, we would have Δ_{∞} ⊢ ∃x : ϕ.¬P, and since Δ_{∞} is a Henkin theory, Δ_{∞} ⊢ ¬P [t] for some Γ ⊢ t : ϕ, which contradicts the above.

Conversely, suppose Δ_{∞} ⊢ ∀x : ϕ.P. Now let [u] ∈ ⟦ϕ⟧. We cannot use completeness to infer that u : ϕ but we do get Δ_{∞} ⊢ u ∼ ϕ, that is, there exists t : ϕ such that u ≃_{ϕ} t, and so ⟦u⟧ =_{⟦ϕ⟧} ⟦t⟧.

Now by (∀-ELIM), Δ_{∞} ⊢ P [t] so by the inductive hypothesis, A ⊨ P [t], and by Lemma 5.2, A ⊨ P [u]. Hence A ⊨ ∀x : ϕ.P.

• A ⊨ F (t) when ⟦t⟧ ⊆ Pred(F). Now predicates only apply to typable terms, so t : σ say. Although t might not be total, for all u ∈ Total(t), u =_{σ} t. By definition of u ∈ Pred(F) in the term model, Δ_{∞} ⊢ F (u), so by CONG, Δ_{∞} ⊢ F (t). Conversely, if Δ_{∞} ⊢ F (t), then Δ_{∞} ⊢ F (u) for all u ∈ Total(t), so ⟦t⟧ ⊆ Pred(F).

• A ⊨ t =_{ϕ} t′ is t ≃_{ϕ} t′, in other words, for all u ∈ Total(t) and u′ ∈ Total(t′), we have u ∼_{ϕ} u′.

We must show that t ≃_{ϕ} t′ ⟺ Δ_{∞} ⊢ t =_{ϕ} t′. Recall that we have assumed t, t′ : ϕ for well-formedness of the proposition t =_{ϕ} t′.

– For all Γ ⊢ t, t′ : 1 we have t ≃_{1} t′ and Γ ⊢ t =_{1} t′.

– Suppose Δ_{∞} ⊢ t =_{γ} t′. Then since Δ_{∞} ⊢ g ≃_{Γ} Γ (with the obvious meaning), and since ≃ is a congruence (Proposition 3.5), we have Δ_{∞} ⊢ t[g/Γ] ≃_{γ} t′[g/Γ], so A ⊨ t[g/Γ] =_{γ} t[g/γ]. Since ⟦t⟧ = ⟦t′[g/Γ]⟧, and ⟦t′⟧ = ⟦t′[g/Γ]⟧, we get A ⊨ t =_{γ} t′. Conversely, suppose t ≃_{γ} t′. Now Δ must contain the proposition x = ĝ_{x} for each x in Γ. Then, since closed t[ĝ/Γ] : γ, we can deduce by Proposition 3.2 that there exists some total t′′ such that u ∈ Total(t[ĝ/Γ]) ⇒ u =_{γ} t′′. Hence Δ_{∞} ⊢ t[ĝ/Γ] =_{γ} t′′ and similarly, Δ_{∞} ⊢ t′[ĝ/Γ] =_{γ} t′′. We get the same t′′ since t[ĝ/Γ] ≃_{γ} t′[ĝ/Γ] (using Proposition 3.5). Then since Δ_{∞} ⊢ t =_{γ} t[ĝ/Γ] and Δ_{∞} ⊢ t′ =_{γ} t′[ĝ/Γ], we get Δ_{∞} ⊢ t =_{γ} t′.

– Suppose t ≃_{Σ_{x:ϕ}ψ} t′. We prove that π_{2}(t) ≃_{ψ[π_{1}(t)]} π_{2}(t′).

Suppose u_{2} ∈ π_{2}(t), u′_{2} ∈ π_{2}(t′). Then there exist u_{1}, u′_{1} such that ⟨u_{1}, u_{2}⟩ ∼_{Σ_{x:ϕ}ψ} ⟨u′_{1}, u′_{2}⟩, so u_{2} ∼_{ψ[u_{1}]} u′_{2}. Since u_{1} ∈ Total(π_{1}(t)), by soundness of π_{1}(t) : ϕ, u_{1} ≃_{ϕ} π_{1}(t), so by Lemma 5.2, u_{2} ∼_{ψ[π_{1}(t)]} u′_{2}. Hence, π_{2}(t) ≃_{ψ[π_{1}(t)]} π_{2}(t′). Similarly, we can show that π_{1}(t) ≃_{ϕ} π_{1}(t′) By induction, this is equivalent to π_{1}(t) =_{ϕ} π_{1}(t′) and π_{2}(t) =_{ψ[π_{1}(t)]} π_{2}(t′), and so Δ_{∞} ⊢ t =_{Σ_{x:ϕ}ψ} t′.

– First note that t_{1} =_{Π_{x:ϕ}ψ} t′_{1} ⟺ for all t_{2}, t′_{2} : ϕ, t_{2} =_{ϕ} t′_{2} ⊃ t_{1}t_{2} =_{ψ[t_{1}]} t′_{1}t′_{2}.

Now suppose t_{1} ≃_{Π_{x:ϕ}ψ} t′_{1}, that is, for all u_{1} ∈ Total(t_{1}), u′_{1} ∈ Total(t′_{1}), u_{1} ∼_{Π_{x:ϕ}ψ} u′_{1}. Then if t_{2} =_{ϕ} t′_{2}, for u_{2} ∈ Total(t_{2}), u′_{2} ∈ Total(t′_{2}), we have u_{2} ∼_{ϕ} u′_{2}, so App(u_{1}, u_{2}) ∼_{ψ[u_{1}]} App(u′_{1}, u′_{2}), so by Lemma 5.2, App(u_{1}, u_{2}) ∼_{ψ[t_{1}]} App(u′_{1}, u′_{2}). By the inductive hypothesis, t_{1}t_{2} =_{ψ[t_{1}]} t′_{1}t′_{2}. Thus, for all t_{2} =_{ϕ} t′_{2}, t_{1}t_{2} =_{ψ[t_{1}]} t′_{1}t′_{2}, and so t_{1} =_{Π_{x:ϕ}ψ} t′_{1}.

– Suppose t ≃_{(x:ϕ)P} t′. So for all u ∈ Total(t), u′ ∈ Total(t′), u ∼_{(x:ϕ)P} u′. Therefore u ∼_{ϕ} u′, and by the inductive hypothesis, t =_{ϕ} t′. Now in assuming well-formedness, we have t, t′ : (x : ϕ)P and so by CONG-EQ, t =_{(x:ϕ)P} t′.

• A ⊨ ϕ ⊑ ϕ′

If ϕ′ is inhabited then x : ϕ′ ∈ Γ_{∞} so Δ_{∞} ⊢ x : ϕ′ and we can deduce (see Remark 3.2) that Δ_{∞} ⊢ ϕ ⊑ ϕ′.

If ϕ′ is not inhabited we can prove Δ_{∞} ⊢ ϕ ⊑ ϕ′ directly. Now to say that ϕ′ is uninhabited is to say that there does not exist a closed term t : ϕ′. Since Δ is a maximally consistent Henkin extension, we must have ¬∃x : ϕ′.true ∈ Δ. Hence Δ_{∞}, x : ϕ′ ⊢ false. Hence by (REFTYPE-L-REF), Δ_{∞} ⊢ (x : ϕ′)false ⊑ ϕ′. Now Proposition 3.4 gives us Δ_{∞} ⊢ ϕ ⊑ (x : ϕ′)false and so using (TRANS-REF) Δ_{∞} ⊢ ϕ ⊑ ϕ′.

Conversely, if Δ_{∞} ⊢ ϕ ⊑ ϕ, then using Proposition 3.1 and the inductive hypothesis on ϕ and ϕ′, we get A ⊨ ϕ ⊑ ϕ′.

• A ⊨ t : ϕ, i.e. t ≃_{ϕ} t′. We show Δ_{∞} ⊢ t ∼ ϕ, that is, there exists Δ_{∞} ⊢ t′ : ϕ such that t ≃_{ϕ} t′.

– A ⊨ t : 1 when for all u, u′ ∈ Total(t), Δ_{∞} ⊢ u ∼_{1} u′, so u =1 u′. Hence for any u ∈ Total(t), we have t ≃_{1} u : 1, and so Δ_{∞} ⊢ t ∼ 1.

– The A ⊨ t : γ case is similar to that of 1.

– If t ≃_{Σ_{x:ϕ}ψ} t, then using reasoning similar to the t =_{Σ_{x:ϕ}ψ} t′ case above, π_{1}(t) ≃_{ϕ} π_{1}(t) and π_{2}(t) ≃_{ψ[π_{1}(t)]} π_{2}(t). By the inductive hypothesis, we get some t′_{1} such that π_{1}(t) ≃_{ϕ} t′_{1} : ϕ, and t′_{2} such that π_{2}(t) ≃_{ψ[π_{1}(t)]} t′_{2}. Using Lemma 5.2, we deduce that π_{2}(t) ≃_{ψ[t′_{1}]} t′_{2}. Hence, t ≃_{Σ_{x:ϕ}ψ} ⟨t′_{1}, t′_{2}⟩, and so ⟨t′_{1}, t′_{2}⟩ ∼ Σ_{x:ϕ}ψ.

– A ⊨ t : Π_{x:ϕ}ψ. Suppose ϕ is inhabited. Then x : ϕ ∈ Γ_{∞} so A ⊨ tx : ψ, and by induction, there exists a t′ : ψ such that tx ≃_{ψ} t′. Hence Δ_{∞} ⊢ t ≃_{Π_{x:ϕ}ψ} λx : ϕ.t′ and Δ_{∞} ⊢ t : Π_{x:ϕ}ψ. If ϕ is not inhabited, then we can prove Δ_{∞} ⊢ t : Π_{x:ϕ}ψ directly (which implies t ∼ Π_{x:ϕ}ψ). Since t must be well-structured for its interpretation to be well-defined, we can use Proposition 3.3.

– A ⊨ t : (x : ϕ)P ⟺ A ⊨ t : ϕ and A ⊨ P [t]. The ⇒ follows from Lemma 5.3. For ⇐, use soundness of x : ϕ ⊢ P wf and t : ϕ. Then, since ϕ < (x : ϕ)P, there exists t′ : ϕ such that t ≃_{ϕ} t′. By Lemma 5.2, A ⊨ P [t′]. Now we assumed Γ ⊢ (x : ϕ)P wf and Γ ⊢ t : ϕ, so Γ ⊢ P [t′] wf, and since P [t′] < (x : ϕ)P, we get Δ_{∞} ⊢ P [t′]. Hence Δ_{∞} ⊢ t′ : (x : ϕ)P, and Δ_{∞} ⊢ t ∼ (x : ϕ)P.

Corollary 5.1 The calculus is a conservative extension of λ^{×→}: If Γ ⊢ t =_{τ} t′ is a well-formed equation in λ^{×→}, then it is provable in λ^{×→}, if and only if it is provable in the calculus of refinement types.

Proof: Both calculi are complete for the class of Henkin Models. Similarly,

Corollary 5.2 The calculus is a conservative extension of first-order logic : If Γ ⊢ P wf does not contain any refinement types, then it is provable in first-order logic, if and only if it is provable in the calculus of refinement types.

Proof: Both systems are complete for the class of Henkin Models.

The significance of these corollaries is that we are free to use the specification language for proving program equivalences, and for reasoning about programs using the program logic, in the knowledge that it faithfully reflects the equality in the underlying programming language, and proofs in the program logic.

6 Conclusions

We have described the refinement type methodology of specification. This is a way of combining the type system of a programming language with a program logic to give a specification language. This is an alternative to approaches which rely on encoding a logic into an expressive type theory, and those which simply use a program logic.

The two-level nature of the calculus suggests the construction of a modular tool in which checking program correctness is a combination of type checking and theorem proving. The modularity would come from constructing a ‘specification checker’ from an existing theorem prover and a type checker, for the program logic and programming language respectively. Indeed, this is similar to what is done in the interactive proof development systems, Nuprl and PVS.

The calculus could provide a foundation for other specification based formalisms. In the proof that div2 satisfied its specification we used the proof for div2′. There is an implicit element of refinement here. We envisage separate extensions to transformation and refinement calculi, and an embedding in a calculus of full program annotations.

Although we give a refinement relation ϕ ⊑ ϕ′ on specifications, this does not constitute a full refinement calculus (such as in [Mor94]). The idea there is to internalise specifications into programs and consider a refinement relation on mixtures of specification and program. This is carried out in the author’s forthcoming PhD thesis. The structure imposed on specifications would help to partially automate verification and derivation.

By extending the type system of λ^{×→} to refinement types, we gain a simple notion of program annotation, where variables on abstractions are labelled with logical information. Expressing local contextual information is useful, as we often need to be able to make use of facts which are true at some point in a program. For example, if it is known that variable n must be within certain bounds, then a programmer (or compiler) may be able to perform some partial evaluation or optimisation.

The ability to express equality at a refinement type is useful in program transformation. For example, we might want to transform a function of type nat → nat, with the prescription “maintain value on evens, and improve on odds (in some way)”. We can express (part of) this by saying that the terms are equal at the refinement type even → nat.

This account of specifications which brings equality to the fore should be especially useful in data refinement, where it is natural to consider different equalities at the abstract and concrete types.

We believe that the principles outlined here are general enough to be applied to structures other than those traditionally studied — data flow diagrams for example. Since the logic is arbitrary (up to a point) we are not constrained by the type theory. It would be an interesting line of research to see how type-theoretic and semantic ideas could help there.

Acknowledgements

This work has benefited from discussions with my supervisors — Gordon Plotkin, John Power and Marcelo Fiore. Conversations with Alex Bunkenburg, Healfdene Goguen and James McKinna have also been useful.

References

[Asp95] David Aspinall. Subtyping with singleton types. In Proceedings of Computer Science Logic ‘94, volume 933 of LNCS, 1995.

[BM92] R. Burstall and J. McKinna. Deliverables : a categorical approach to program construction in type theory. LFCS Technical Report ECS-LFCS-92-242, Department of Computer Science, University of Edinburgh, 1992.

[Bur92] G.L. Burn. A logical framework for program analysis. In J. Launchbury and P. Sansom, editors, Proceedings of the 1992 Glasgow Functional Programming Workshop, pages 30–42. Springer-Verlag Workshops in Computer Science series, 6–8 July 1992.

[Fef85] Solomon Feferman. A theory of variable types. Revista Colombiana de Matématicas, 19, 1985.

[FP91] Tim Freeman and Frank Pfenning. Refinement types for ML. In Proceedings of the SIG-PLAN’91 Symposium on Language Design and Implementation, pages 268–277. ACM Press, 1991.

[Hay94a] Susumu Hayashi. Logic of refinement types. In Types for Proofs and programs, volume 806 of Lecture Notes in computer Science. Springer Verlag, 1994.

[Hay94b] Susumu Hayashi. Singleton, union, and intersection types for program extraction. Information and Computation, 109:174–210, 1994.

[Jen91] Thomas Jensen. Strictness analysis in logical form. In J. Hughes, editor, Proceedings of the Conference on Functional Programming and Computer Architecture, volume 523 of LNCS, pages 352–366, 1991.

[Luo91] Z. Luo. Program specification and data refinement in type theory. LFCS Technical Report ECS-LFCS-90-131, Department of Computer Science, University of Edinburgh, 1991.

[McK92] James McKinna. Deliverables : A Categorical Approach to Program Development in Type Theory. PhD thesis, Department of Computer Science, University of Edinburgh, 1992.

[Mit96] J. Mitchell. Foundations for Programming Languages. Foundations of Computing Series. MIT Press, 1996.

[Mor94] C. Morgan. Programming from Specifications. Prentice Hall, 1994.

[NN88] Hanne Nielson and Flemming Nielson. Automatic binding time analysis for a typed λ-calculus. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, 1988.

[NPS90] B. Nordström, K. Petersson, and J.M. Smith. Programming in Martin-Löf’s Type Theory, volume 7 of Monographs on Computer Science. Oxford University Press, 1990.

[Pfe93] Frank Pfenning. Refinement types for logical frameworks. In Herman Geuvers, editor, Informal Proceedings of the Workshop on Types for Proofs and Programs, pages 285–299, 1993.

[vD94] Dirk van Dalen. Logic and Structure. Springer-Verlag, 1994.

A RULES OF THE CALCULUS 19

A Rules of the calculus

⊢ ⟨⟩ wf  (EMPTY-WF)
{Γ ⊢ ϕ wf \atop ⊢ Γ, x : ϕ wf} x ∉ Γ  (VARCON-WF)
{Γ ⊢ P wf \atop ⊢ Γ, P wf}  (PROPCON-WF)

Figure 1: Well-formedness of contexts

{⊢ Γ wf \atop Γ ⊢ 1 : Ref 1}  (1-WF)
Γ ⊢ ϕ : Ref σ Γ, x : ϕ ⊢ ψ : Ref τ

Γ ⊢ Σ_{x:ϕ}ψ : Ref σ × τ (Σ-WF)

Γ ⊢ ϕ : Ref σ Γ, x : ϕ ⊢ ψ : Ref τ

Γ ⊢ Π_{x:ϕ}ψ : Ref σ → τ (Π-WF)

Γ ⊢ ϕ : Ref τ Γ, x : ϕ ⊢ P wf

Γ ⊢ (x : ϕ)P : Ref τ (REFTYPE-WF)

{⊢ Γ wf \atop Γ ⊢ γ : Ref γ} (γ primitive)  (PRIMTYPE-WF)

Figure 2: Well-formedness of refinement types

        ⊢ Γ wf ; Γ ⊢ false wf  (false-WF)

Γ ⊢ P wf Γ ⊢ P′ wf
Γ ⊢ P ⊃ P′ wf (⊃-WF)

{Γ, x : ϕ ⊢ P wf \atop Γ ⊢ ∀x : ϕ.P wf}  (∀-WF)

{Γ ⊢ t_{i} : τ_{i} \atop Γ ⊢ F (t_{1}, …, t_{n}) wf}  (F : pred τ_{1}, …, τ_{n}) (PRED-WF)

\begin{matrix}Γ ⊢ t : ϕ & Γ ⊢ t′ : ϕ \\ Γ ⊢ t =_{ϕ} t′ wf \end{matrix}  (=-WF)
Γ ⊢ ϕ : Ref τ Γ ⊢ ϕ′ : Ref τ
Γ ⊢ ϕ ⊑ ϕ′ wf (⊑-WF)

Figure 3: Well-formedness of propositions

{⊢ Γ, x : ϕ, Γ′ wf \atop Γ, x : ϕ, Γ′ ⊢ x : ϕ}  (VAR)

{Γ ⊢ t_{i} : τ_{i} \atop Γ ⊢ k(t_{1}, …, t_{n}) : τ} (k : τ_{1}, …, τ_{n} → τ primitive)  (CONST)

{⊢ Γ wf \atop Γ ⊢ ∗ : 1}  (UNIT)

\begin{aligned}Γ ⊢ t : ϕ & Γ ⊢ t′ : ψ[t/x] & Γ, x : ϕ ⊢ ψ wf \\ & Γ ⊢ ⟨t, t′⟩ : Σ_{x:ϕ}ψ \end{aligned}  (PAIR)

{Γ, x : ϕ ⊢ t : ψ \atop Γ ⊢ λx : ϕ.t : Π_{x:ϕ}ψ}  (ABS)

{Γ ⊢ t : Σ_{x:ϕ}ψ \atop Γ ⊢ π_{1}(t) : ϕ}  (PROJ1)

{Γ ⊢ t : Σ_{x:ϕ}ψ \atop Γ ⊢ π_{2}(t) : ψ[π_{1}(t)/x]}  (PROJ2)

\begin{matrix}Γ ⊢ t : Π_{x:ϕ}ψ & Γ ⊢ t′ : ϕ \\ Γ ⊢ tt′ : ψ[t′/x] \end{matrix}  (APP)

\begin{matrix}Γ ⊢ t : ϕ & Γ ⊢ P [t/x] \\ Γ ⊢ t : (x : ϕ)P \end{matrix}  (REFTYPE-INTRO)

{Γ ⊢ t =_{ϕ} t′ \atop Γ ⊢ t : ϕ}  (EQ)

\begin{matrix}Γ ⊢ t : ϕ′ & Γ ⊢ ϕ ⊑ ϕ′ \\ Γ ⊢ t : ϕ \end{matrix}  (WEAKEN)

Figure 4: Refinement typings

\begin{matrix}Γ, x : ϕ ⊢ t : ψ & Γ ⊢ t′ : ϕ \\ Γ ⊢ (λx : ϕ.t)t′ =_{ψ[t′/x]} t[t′/x] \end{matrix}  (λ-β-EQ)

{Γ, x : ϕ ⊢ tx : ψ \atop Γ ⊢ λx : ϕ.tx =_{Π_{x:ϕ}ψ} t} x ∉ t  (λ-η-EQ)

\begin{matrix}Γ ⊢ t_{1} : ϕ_{1} & Γ ⊢ t_{2} : ϕ_{2} \\ Γ ⊢ π_{i}⟨t_{1}, t_{2}⟩ =_{ϕ_{i}} t_{i} \end{matrix}  (π-β-EQ)

\begin{matrix}Γ ⊢ π_{1}(t) : ϕ & Γ ⊢ π_{2}(t) : ψ[π_{1}(t)/x] \\ Γ ⊢ ⟨π_{1}(t), π_{2}(t)⟩ =_{Σ_{x:ϕ}ψ} t \end{matrix}  (π-η-EQ)

{Γ ⊢ t : 1 \atop Γ ⊢ t =_{1} ∗}  (∗-η-EQ)

Figure 5: βη equality rules

Γ ⊢ t =_{ϕ} t′  (Ax ▷ Γ ⊢ t =_{ϕ} t′) (AXIOM-EQ)

\begin{matrix}Γ ⊢ ϕ′ ⊑ ϕ & Γ, x : ϕ ⊢ t =_{ψ} t′ \\ Γ ⊢ λx : ϕ.t =_{Π_{x:ϕ}ψ} λx : ϕ′.t′ \end{matrix}  (ABS-ξ-EQ)

\begin{matrix}Γ ⊢ t_{1} =_{Π_{x:ϕ}ψ} t′_{1} & Γ ⊢ t_{2} =_{ϕ} t′_{2} \\ Γ ⊢ t_{1}t_{2} =_{ψ[t_{2}/x]} t′_{1}t′_{2} \end{matrix}  (APP-ξ-EQ)

\begin{matrix}Γ ⊢ t_{1} =_{ϕ} t′_{1} & Γ ⊢ t_{2} =_{ψ[t_{1}/x]} t′_{2} \\ Γ ⊢ ⟨t_{1}, t_{2}⟩ =_{Σ_{x:ϕ}ψ} ⟨t′_{1}, t′_{2}⟩ \end{matrix}  (PAIR-ξ-EQ)

{Γ ⊢ t =_{Σ_{x:ϕ}ψ} t′ \atop Γ ⊢ π_{1}(t) =_{ϕ} π_{1}(t′)}  (PROJ1-ξ-EQ)

{Γ ⊢ t =_{Σ_{x:ϕ}ψ} t′ \atop Γ ⊢ π_{2}(t) =_{ψ[π_{1}(t)/x]} π_{2}(t′)}  (PROJ2-ξ-EQ)

{Γ ⊢ t : ϕ \atop Γ ⊢ t =_{ϕ} t}  (REFL-EQ)

\begin{aligned}Γ ⊢ t =_{ϕ} t′ & Γ ⊢ P [t/x] & Γ, x : ϕ ⊢ P wf \\ & Γ ⊢ t =_{(x:ϕ)P} t′ \end{aligned}  (CONG-EQ)

{Γ ⊢ t =_{ϕ} t′ \atop Γ ⊢ t′ =_{ϕ} t}  (SYMM-EQ)

\begin{matrix}Γ ⊢ t =_{ϕ} t′ & Γ ⊢ t′ =_{ϕ} t′′ \\ Γ ⊢ t =_{ϕ} t′′ \end{matrix}  (TRANS-EQ)

Figure 6: Other equalities

{⊢ Γ wf \atop Γ ⊢ 1 ⊑ 1}  (1-REF)

\begin{matrix}Γ ⊢ ϕ ⊑ ϕ′ & Γ, x : ϕ ⊢ ψ ⊑ ψ′ \\ Γ ⊢ Σ_{x:ϕ}ψ ⊑ Σ_{x:ϕ′}ψ′ \end{matrix}  (Σ-REF)

\begin{matrix}Γ ⊢ ϕ′ ⊑ ϕ & Γ, x : ϕ ⊢ ψ ⊑ ψ′ \\ Γ ⊢ Π_{x:ϕ}ψ ⊑ Π_{x:ϕ′}ψ′ \end{matrix}  (Π-REF)

\begin{matrix}Γ ⊢ ϕ ⊑ ψ & Γ, x : ψ ⊢ P \\ Γ ⊢ (x : ϕ)P ⊑ ψ \end{matrix}  (REFTYPE-L-REF)

{Γ, x : ψ, Q ⊢ x : ϕ \atop Γ ⊢ ϕ ⊑ (x : ψ)Q}  (REFTYPE-R-REF)

\begin{matrix}Γ ⊢ ϕ ⊑ ϕ′ & Γ ⊢ ϕ′ ⊑ ϕ′′ \\ Γ ⊢ ϕ ⊑ ϕ′′ \end{matrix}  (TRANS-REF)

Figure 7: Refinement rules

{Γ ⊢ P wf \atop Γ ⊢ P}  (Ax ▷ Γ ⊢ P)  (AXIOM)

\begin{matrix}Γ ⊢ P & Γ ⊢ Q \\ Γ ⊢ P ∧ Q \end{matrix}  (∧-INTRO)

{Γ ⊢ P ∧ Q \atop Γ ⊢ P}  (∧-ELIM1)

{Γ ⊢ P ∧ Q \atop Γ ⊢ Q}  (∧-ELIM2)

{Γ ⊢ P \atop Γ ⊢ P ∨ Q}  (∨-INTRO1)

{Γ ⊢ Q \atop Γ ⊢ P ∨ Q}  (∨-INTRO2)

\begin{aligned}Γ ⊢ P ∨ Q & Γ, P ⊢ R & Γ, Q ⊢ R \\ & Γ ⊢ R \end{aligned}  (∨-ELIM)

{Γ, P ⊢ Q \atop Γ ⊢ P ⊃ Q}  (⊃-INTRO)

\begin{aligned}Γ ⊢ P & Γ ⊢ P ⊃ Q \\ & Γ ⊢ Q \end{aligned}  (⊃-ELIM)

\begin{matrix}Γ ⊢ ∀x : ϕ.P & Γ ⊢ t : ϕ \\ Γ ⊢ P [t/x] \end{matrix}  (∀-ELIM)

{Γ, x : ϕ ⊢ P \atop Γ ⊢ ∀x : ϕ.P}  (∀-INTRO)

Γ ⊢ P wf ; Γ, false ⊢ P  (false-ELIM)

{Γ, ¬P ⊢ false \atop Γ ⊢ P}  (¬-ELIM)

{Γ ⊢ P wf \atop Γ, P ⊢ P}  (HYP)

\begin{aligned}Γ ⊢ t =_{ϕ} t′ & Γ, x : ϕ ⊢ P wf & Γ ⊢ P [t/x] \\ & Γ ⊢ P [t′/x] \end{aligned}  (CONG)

{Γ ⊢ t : (x : ϕ)P \atop Γ ⊢ P [t/x]}  (REFTYPE-ELIM)

Figure 8: Natural Deduction rules for classical first order logic

B Interpretation in Henkin models

a ⟦Γ ⊢ 1 : Ref 1⟧(g) a′ ⟺ a, a′ ∈ A^{1}
⟦Γ ⊢ ϕ : Ref σ⟧ = R ⟦Γ, x : ϕ ⊢ ψ : Ref τ⟧ = S
a ⟦Γ ⊢ Σ_{x:ϕ}ψ : Ref σ × τ⟧(g) a′ ⟺ Proj_{1}^{σ,τ} (a) Rg Proj_{1}^{σ,τ} (a′) and Proj_{2}^{σ,τ} (a) S⟨g, Proj_{1}^{σ,τ} (a)⟩ Proj_{2}^{σ,τ} (a′)
⟦Γ ⊢ ϕ⟧ = R ⟦Γ, x : ϕ ⊢ ψ⟧ = S
f ⟦Γ ⊢ Π_{x:ϕ}ψ⟧(g) f′ ⟺ for all a Rg a′, App(f, a) S⟨g, a⟩ App(f′, a′)
⟦Γ ⊢ ϕ : Ref σ⟧ = R ⟦Γ, x : ϕ ⊢ P wf⟧ = A
a ⟦Γ ⊢ (x : ϕ)P : Ref σ⟧(g) a′ ⟺ a Rg a′, ⟨g, a⟩ ∈ A, ⟨g, a′⟩ ∈ A
a ⟦Γ ⊢ γ : Ref γ⟧(g) a′ ⟺ a, a′ ∈ A^{γ} and a = a′

Figure 9: Interpretation of refinement types

⟦Γ, x : ϕ, Γ′ ⊢ x⟧⟨g, a, g′⟩ = {a} ⟦Γ ⊢ k⟧(g) = {Const(k)}

⟦Γ ⊢ ∗⟧(g) = A^{1}
⟦Γ ⊢ t⟧ = m ⟦Γ ⊢ t′⟧ = m′

⟦Γ ⊢ ⟨t, t′⟩⟧(g) = {a ∈ A^{σ×τ} | Proj_{1}^{σ,τ} (a) ∈ mg, Proj_{2}^{σ,τ} (a) ∈ m′g}

{⟦Γ, x : ϕ ⊢ t⟧ = m \atop ⟦Γ ⊢ λx : ϕ.t⟧(g) = \{f ∈ A^{σ→τ} | ∀a ∈ ⟦Γ ⊢ ϕ⟧(g).App(f, a) ∈ m⟨g, a⟩\}}

{⟦Γ ⊢ t⟧ = m \atop ⟦Γ ⊢ π_{1}(t)⟧(g) = \{Proj_{1}^{σ,τ} (a) | a ∈ mg\}}

{⟦Γ ⊢ t⟧ = m \atop ⟦Γ ⊢ π_{2}(t)⟧(g) = \{Proj_{2}^{σ,τ} (a) | a ∈ mg\}}

\begin{matrix}⟦Γ ⊢ t⟧ = m & ⟦Γ ⊢ t′⟧ = m′ \\ ⟦Γ ⊢ tt′⟧(g) = \{App(f, a) | f ∈ mg, a ∈ m′g\} \end{matrix}

Figure 10: Interpretation of raw terms

⟦Γ ⊢ false⟧ = ∅
⟦Γ ⊢ P ⊃ P′⟧ = {g ⊨ Γ | g ∉ ⟦Γ ⊢ P ⟧ or g ∈ ⟦Γ ⊢ P′⟧}
⟦Γ ⊢ ∀x : ϕ.P ⟧ = {g ⊨ Γ | ∀a ∈ ⟦Γ ⊢ ϕ⟧(g).⟨g, a⟩ ∈ ⟦Γ, x : ϕ ⊢ P ⟧}

{⟦Γ ⊢ t⟧ = m \atop ⟦Γ ⊢ F (t)⟧ = \{g ⊨ Γ | mg ⊆ Pred(F)\}}

\begin{matrix}⟦Γ ⊢ t⟧ = m & ⟦Γ ⊢ t′⟧ = m′ & ⟦Γ ⊢ ϕ⟧ = R \\ ⟦Γ ⊢ t =_{ϕ} t′⟧ = \{g ⊨ Γ | ∀a ∈ mg.∀a′ ∈ m′g . a Rg a′\} \end{matrix}

\begin{matrix}⟦Γ ⊢ ϕ⟧ = R & ⟦Γ ⊢ ϕ′⟧ = R′ \\ ⟦Γ ⊢ ϕ ⊑ ϕ′⟧ = \{g ⊨ Γ | Rg ⊇ R′g\} \end{matrix}

Figure 11: Interpretation of propositions