# Explicit Refinement Types

Jad Elkhaleq Ghalayini  University of CambridgeDepartment of Computer Science
and TechnologyCambridgeUnited Kingdom<EMAIL_ADDRESS>and  Neel
Krishnaswami  University of CambridgeDepartment of Computer Science and
TechnologyCambridgeUnited Kingdom<EMAIL_ADDRESS>
(2023; 2023-03-01; 2023-06-27)

###### Abstract.

We present $\lambda_{\mathsf{ert}}$, a type theory supporting refinement types
with _explicit proofs_. Instead of solving refinement constraints with an SMT
solver like DML and Liquid Haskell, our system requires and permits
programmers to embed proofs of properties within the program text, letting us
support a rich logic of properties including quantifiers and induction. We
show that the type system is sound by showing that every refined program
erases to a simply-typed program, and by means of a denotational semantics, we
show that every erased program has all of the properties demanded by its
refined type. All of our proofs are formalised in Lean 4.

Refinement Types, First Order Logic, Denotational Semantics

††copyright: rightsretained††doi: 10.1145/3607837††journalyear:
2023††submissionid: icfp23main-p19-p††journal: PACMPL††journalvolume:
7††journalnumber: ICFP††article: 195††publicationmonth: 8††ccs: Theory of
computation Program verification††ccs: Theory of computation Denotational
semantics

##  1\. Introduction

Refinement typing extends an underlying type system with the ability to
associate types with logical predicates on their inhabitants, constructing,
for example, the type of nonempty lists or integers between three and seven.
Most such systems support type dependency between the input and output types
of functions, allowing us to give specifications like ”the output of this
function is the type of integers greater than the input.” The core concept
underlying type checkers for refinement types is that of logical entailment.
If we have a value satisfying a predicate $P$ and require a value satisfying
$Q$, we require that $P$ entails $Q$ for our program to typecheck; this then
reduces the typechecking problem to typechecking in our underlying type system
plus discharging a set of entailment obligations, called our verification
conditions. Given an appropriate choice of logic for our predicates, SMT
solvers provide a highly effective way of automatically discharging
verification conditions: this allows us to use refinement types without
dealing with the bookkeeping details required by manual proofs. Combined with
type and annotation inference (in which we also infer refinements), refinement
types allow verifying nontrivial properties of complex programs with a minimal
annotation burden, making them more appealing for use as part of a practical
software development workflow — for example, the Liquid Types implementation
of refinement typing for ML required a manual annotation burden of 1% to prove
the DML array benchmarks safe (Rondon et al., 2008; Xi and Pfenning, 1998).

However, refinement typing’s reliance on automation is a double-edged sword:
while it makes refinement types practical for usage in real-world contexts, it
also creates a hard ceiling for expressiveness, especially if we want to use
quantifiers, which would make the SMT problem undecidable. Rather than
carefully massaging annotations into forms satisfying the particular SMT
solver that is in use, it makes sense to let programmers provide manual proofs
for the (hopefully, few) cases where the solver gets stuck: in utopia, humans
would prove interesting things, and machines would handle the bookkeeping.

However, it is nontrivial to figure out how to add explicit proofs into a
system, because the semantics of refinement type systems is subtle. So before
we can add the capability to move freely between explicit proofs and
automation, we need to know what manual proofs should look like! To achieve
this goal, we introduce a system of explicit refinement types,
$\lambda_{\mathsf{ert}}$, in which all proofs are manual, to explore the
design space. Since our proofs are entirely manual, our refinement logic can
be extremely rich, and, in particular, we support full first-order logic with
quantifiers.

While the presence of explicit proofs means that functions and propositions
look dependently typed, $\lambda_{\mathsf{ert}}$ is not a traditional
dependent type theory. In particular, we maintain the refinement discipline
that ”fancy types” can always be erased, leaving behind a simply-typed
skeleton. Furthermore, $\lambda_{\mathsf{ert}}$ has no judgemental equality –
there is no reduction in types.

Contributions

  * •

We take a simply-typed effectful lambda calculus, $\lambda_{\mathsf{stlc}}$
(in section 5.1), and add a refinement type discipline to it, to obtain the
$\lambda_{\mathsf{ert}}$ language (in Section 4).

  * •

We support a rich logic of properties, including full first-order quantifiers,
as well as ghost variables/arguments (see section 4.2). It does not rely on
automated proof, and instead features _explicit_ proofs of all properties.

  * •

We show (in section 4.3) that this type system satisfies the expected
properties of a type system, such as the syntactic substitution property.

  * •

In section 5, we give a denotational semantics for both the simply-typed and
refined calculi, and we prove the soundness of the intepretations. Using this,
we establish semantic regularity of typing, which shows that every program
respects the refinement discipline.

  * •

We describe our mechanization of the semantics and proofs in Lean 4 in section
6. The proofs are available in the supplementary material.

##  2\. Refinement Types

###  2.1. Pragmatics of Refinement Types

Consider a simply-typed functional programming language. In many cases, the
valid inputs for a function are not the entire input type but rather a subset
of the input; for example, consider the classic function head : List A $\to$
A.

Note that we cannot define this as a total function for an arbitrary type $A$;
we must either provide a default value, change the return type, or use some
system of exceptions/partial functions.

Refinement types give us native support for types guaranteeing an invariant
about their inhabitants by allowing us to associate a base type with a
predicate. For example, we could represent the types of natural numbers and
nonzero integers (in a Liquid-Haskell-like notation) as:

(1) type Nat = {v: Int | v >= 0} type Nonzero = {v: Int | v <> 0}

We could then write the type signature of division as

(2) div : Int $\to$ {v: Int | v <> 0} $\to$ Int

By allowing dependency, where the output type of a function is allowed to
depend on the value of its arguments, we can use such functionality to encode
the specification of operations as well, as in

(3) eq : x:Int $\to$ y:Int $\to$ {b: Bool | (x = y) = b}

Note that these types all use equality and inequality. This is not the
_judgemental_ equality of dependent type theory, but rather a _propositional_
equality that can occur inside types. We could now attempt to implement a
safe-division function on the natural numbers as follows

(4) $\begin{array}[]{l}\texttt{safeDiv : Nat $\to$ Nat $\to$ Nat}\\\
\texttt{safeDiv}\;n\;m=\mathbf{if}\;\texttt{eq}\;m\;0\;\mathbf{then}\;0\;\mathbf{else}\;\texttt{div}\;n\;m\end{array}$

A refinement type system reduces the problem of type-checking to the question
of whether a set of logical _verification conditions_ holds. In this case, all
of the propositions are decidable. Unfortunately, with more general
specifications, checking these conditions quickly becomes undecidable. For
example, if we permitted equations between arbitrary polynomials, then
Hilbert’s tenth problem – the solution of Diophantine equatiosn – can easily
be encoded. However, by appropriately restricting the logic of assertions, we
can reduce the problem of checking verification conditions to a decidable
fragment of logic that, while NP-hard (or worse), can usually be solved very
effectively in practice.

In particular, many languages supporting refinement types require refinements
to be expressions in the quantifier-free fragment of first-order logic, with
atoms restricted to carefully chosen ground theories with efficient decision
procedures. In Liquid Haskell, for example, formulas in refinements are
restricted to formulas in QF-UFLIA (Vazou et al., 2014): the _quantifier-free_
theory of uninterpreted functions with linear integer arithmetic. While such a
system may, at first glance, seem very limited, it is possible to prove very
sophisticated properties of real programs with it. In particular, with clever
function definitions and termination checking (which generates a separate set
of verification conditions to ensure some measure on recursive calls to a
function decreases), it is even possible to perform proofs by induction in a
mostly-automated fashion (Jhala and Vazou, 2020).

However, it can be challenging to formulate definitions in such a limited
fragment of logic, and many properties (such as monotonicity of functions or
relational composition) require the use of quantifiers to be stated naturally.
Unfortunately, attempts to extend solvers to support more advanced features
like quantifiers usually lead to very unreliable performance.

Another issue is that systems designed around off-the-shelf solvers often do
not satisfy the _de-Bruijn criterion_ : their trusted code-base, rather than
being restricted to a small, easily-trusted kernel, instead will often consist
of an entire solver and associated tooling! Unfortunately, SMT solvers are
incredibly complex pieces of software and hence are very likely to have
soundness bugs, as recent research on fuzzing state-of-the-art solvers like
CVC4 and Z3 for bugs tends to show (Winterer et al., 2020).

In our work, we build a refinement type system, which replaces the use of
automated solvers with explicit proofs. This permits (at the price of writing
proofs) the free use of quantifiers in propositions, while also having a
trusted codebase small enough to be formally verified.

###  2.2. Semantics of Refinement Types

To understand what refinement types are semantically, it is worth recalling
that there are two main styles of doing denotational semantics, which Reynolds
dubbed ”intrinsic” and ”extrinsic” (Reynolds, 2003).

The intrinsic style is the usual style of categorical semantics – we find some
category where types and contexts are objects, and a term $\Gamma\vdash e:A$
is interpreted as an element of the hom-set $\mathrm{Hom}(\Gamma,A)$.
(Dependency does make things more complicated technically, but not in any
conceptually essential fashion.) In the intrinsic style, only well-typed terms
have denotations, and ill-typed terms are grammatically ill-formed and do not
have a semantics at all. Another way of putting this is that intrinsic
semantics interprets _typing derivations_ rather than _terms_.

In the extrinsic style, the interpretation function is defined upon raw terms,
and ill-typed programs _do_ get a semantics. Types are then defined as
retracts of the underlying semantic object interpreting the raw terms. A good
example of this style of semantics is Milner’s proof of type safety for ML in
(Milner, 1978): he gave a denotational semantics for an untyped lambda
calculus, and then gave an interpretation of types by logical relations over
this untyped calculus, which let him use the fundamental lemma to extract type
safety. Logical relations (and realizabilty methods in general) are typical
examples of extrinsic semantics. Normally type theorists elide the distinction
between these two styles of semantics, because we prove coherence: that the
same term cannot have two derivations with different semantics. This is called
the ”bracketing theorem” in Reynolds (2003) and Melliès and Zeilberger (2015).

Refinement types puts these two styles of semantics together in a different
way. We start with a unrefined, base language with an intrinsic semantics, and
then define a _second_ system of types as a family of retracts over the base
types. In $\lambda_{\mathsf{ert}}$, we use a monadic lambda-calculus as the
base language, and define our system of refinements over this calculus, with
the refinements structured as a fibration over the base calculus. We
deliberately avoided foregrounding the categorical machinery in our paper to
make it more accessible, though we do direct readers to Melliès and Zeilberger
(2015)’s POPL paper (which deeply influenced our design).

Another, perhaps more familiar, instance of this framework are Hoare logic and
separation logic, which can be understood as refinement type systems over a
base ”uni-typed” imperative language. In fact, the distinction in Hoare logic
between ”logical variables” (which appear in specifications) and program
variables is (in semantic terms) precisely the same as the distinction between
logical and computational terms in $\lambda_{\mathsf{ert}}$ – which we will
discuss further in the next section.

##  3\. Explicit refinement types

In this section, we introduce our system of _explicit refinement types_ ,
$\lambda_{\mathsf{ert}}$, which we construct by enriching the simply-typed
lambda calculus with proofs, intersection types, and union types. We recover a
computational interpretation of terms in our calculus by recursively erasing
the logical information added, yielding back simply-typed
$\lambda_{\mathsf{stlc}}$ terms. The presence of proofs allows us to track
logical facts, and by pairing a term with a proof of its property, form subset
types. We also support a general form of intersection and union type, to allow
us to pass around terms used only in proofs in a way that is guaranteed to be
_computationally irrelevant_ , which is both a significant performance concern
and allows type signatures to more clearly express the programmer’s intent.
For example, consider the following definition of a vector type:

(5)
$\mathsf{Vec}\;A\;n\equiv\\{\ell:\mathsf{List}\;A\mid\mathsf{List.len}\;\ell=n\\}$

In particular, we define a vector of length $n$ as a list paired with the
information that the list has length $n$. That is, a vector is a subset type:
a base type $\mathsf{List}\;A$ paired with a proposition $P(\ell)$ (here
$\mathsf{len}\;\ell=n$), which we will interpret as containing all elements
$\ell$ of the base type satisfying $P(\ell)$. In general, we write such types
as $\\{x:X\mid P(x)\\}$, and introduce them with the form $\\{e,p\\}$, where
$e$ is of type $X$ and $p$ is a proof of $P(e)$. We define a length function
on vectors as follows:

(6) $\begin{array}[]{lclll}\mathsf{Vec.len}&:&\forall
n:\mathbb{N},&\mathsf{Vec}\;A\;n\to&\mathbb{N}\\\
\mathsf{Vec.len}&\equiv&\hat{\lambda}\|n:\mathbb{N}\|,&\lambda
v:\mathsf{Vec}\;A\;n,&\mathsf{let}\;\\{\ell,p\\}=v\;\mathsf{in}\;\mathsf{List.len}\;\ell\par\end{array}$

Let us break this definition down, starting from the signature.
$\mathsf{Vec.len}$ begins by universally quantifying over a natural number $n$
with the quantifier $\forall n:\mathbb{N}$, and then has a function type
$\mathsf{Vec}\;A\;n\to\mathbb{N}$. We can interpret this as saying that for
every $n$, $\mathsf{Vec.len}$ takes vectors of length $n$ to a natural number.

The $\forall$ quantifier in the type of $\mathsf{Vec.len}$ behaves like the
quantifiers in ML-style polymorphism, rather than the pi-type of dependent
type theory. It indicates that the _same_ function can handle vectors of any
length, with no explicit branching on the length. In contrast, a pi-type can
lets the function body compute with the natural number argument.

An explicit binding, written $\lambda\|n:\mathbb{N}\|$, represents this
quantifier in the actual definition; we call a variable binding surrounded by
double bars (e.g., $\|x:A\|$) a _ghost binding_. Moving inwards, we have a
function type with input $\mathsf{Vec}\;A\;n$ and output $\mathbb{N}$; this
corresponds to the lambda-expression ”$\lambda v:\mathsf{Vec}\;A\;n,E$” in the
definition, where
$E\equiv\mathsf{let}\;\\{\ell,\\_\\}=v\;\mathsf{in}\;\mathsf{len}\;\ell$ is an
expression of type $\mathbb{N}$. Breaking down $E$, we must first explicitly
destructure our vector $v$ into its components, a list $\ell$ and a proof, $p$
that $\ell$ is of length $n$. Unlike in refinement type systems like DML and
Liquid Haskell, this is explicit, with no entailment-based subtyping.

The definition in equation 6 ignores the proof component of the let-binding
and hence the refinement information carried by our type system. One way to
use the proof information would be to have a definition for
$\mathsf{Vec.len}$, which promises to return an integer equal to the length.

(7) $\begin{array}[]{lclll}\mathsf{Vec.len^{\prime}}&:&\forall
n:\mathbb{N},&(v:\mathsf{Vec}\;A\;n)\to&\\{x:\mathbb{N}\mid x=n\\}\\\
\mathsf{Vec.len^{\prime}}&\equiv{}&\hat{\lambda}\|n:\mathbb{N}\|,&\lambda
v:\mathsf{Vec}\;A\;n,&\mathsf{let}\;\\{\ell,p\\}=v\;\mathsf{in}\;\\{\mathsf{List.len}\;\ell,p\\}\par\end{array}$

However, one helpful feature of $\lambda_{\mathsf{ert}}$ is that even in this
case, we can prove facts about our definitions by writing freestanding proofs
about them rather than cramming every possible fact we could want into our
type signature. For example, we could give a proof a proposition that the
definition in equation 6 is correct as follows:

(8) $\begin{array}[]{ll}\mathsf{Vec.len\\_def}:&\forall n:\mathbb{N},\forall
v:\mathsf{Vec}\;A\;n,\mathsf{Vec.len}\;\|n\|\;v=n\\\
\mathsf{Vec.len\\_def}\equiv{}&\hat{\lambda}\|n:\mathbb{N}\|,\hat{\lambda}\|v:\mathsf{Vec}\;A\;n\|,\mathsf{let}\;\\{\ell,p\\}=v\;\mathsf{in}\\\
&\mathsf{trans}[\mathsf{Vec.len}\;\|n\|\;\\{\ell,p\\}\\\
&\qquad\;{=}(\beta_{\mathsf{ir}})\;(\lambda
v,\mathsf{let}\;\\{\ell,\\_\\}=v\;\mathsf{in}\;\mathsf{List.len}\;\ell)\\{\ell,p\\}\\\
&\qquad\;{=}(\beta_{\mathsf{ty}})\;(\mathsf{let}\;\\{\ell,\\_\\}=\\{\ell,p\\}\;\mathsf{in}\;\mathsf{List.len}\;\ell)\\\
&\qquad\;{=}(\beta_{\mathsf{set}})\;\;\mathsf{List.len}\;\ell\\\
&\qquad\;{=}(p)\;\;n]\end{array}$

Let us break this definition down, again starting with the signature. We
quantify over both the length $n:\mathbb{N}$ and the vector
$v:\mathsf{Vec}\;A\;n$, and then assert the equality proposition
$\mathsf{Vec.len}\;\|n\|\;v=n$. In the proofs, both universal quantifiers are
introduced by ghost lambdas ”$\hat{\lambda}\|n:\mathbb{N}\|$” and
”$\hat{\lambda}\|v:\mathsf{Vec}\;A\;n\|$”. However, we use $\hat{\lambda}$
instead of $\lambda$ because we are proving a universally quantified
_proposition_ rather than forming a _term_ of intersection type. The proof of
equality is a term of the form $\mathsf{trans}[...]$, which represents an
Agda-style syntax sugar for equational reasoning. In particular, if
$\mathsf{trans}_{p,q,r}:p=q\to q=r\to p=r$ is the transitivity rule, then we
have the desugaring

(9)
$\mathsf{trans}[x_{0}\;{=}(p_{0})\;x_{1}\;{=}(p_{1})\;x_{2}\;...\;x_{n}\;{=}(p_{n})\;x_{n+1}]\equiv\mathsf{trans}_{x_{0},x_{1},x_{n}}\;p_{0}(\mathsf{trans}_{x_{1},x_{2},x_{n}}\;p_{1}\;(...))$

where each $p_{i}$ is evidence of the proposition $x_{i}=x_{i+1}$.

Examining the proof of equation 5, we see that every piece of evidence used
except one is of the form ”$\beta_{\mathsf{something}}$”. These are explicit
$\beta$-reduction proofs, which are necessary since our calculus does not
include a notion of judgemental equality: type equality is simply
$\alpha$-equivalence. 111 The actual $\beta$-reduction rules in our calculus,
e.g. $\beta_{\mathsf{ty}}$, require explicit annotations to be unambiguous. We
omit these here for space and clarity.  While this dramatically simplifies the
meta-theory, this can make even simple proofs very long. In our examples, we
implement the pattern of repeatedly applying a $\beta$-reduction as syntactic
sugar. Writing it as $\beta$ (pronounced ”by beta”), we get the much simpler
proof

(10) $\begin{array}[]{ll}\mathsf{Vec.len\\_def}&:\forall n:\mathbb{N},\forall
v:\mathsf{Vec}\;A\;n,\mathsf{len}\;v=n\\\
\mathsf{Vec.len\\_def}&\equiv\hat{\lambda}\|n:\mathbb{N}\|,\hat{\lambda}\|v:\mathsf{Vec}\;A\;n\|,\\\
&\hskip
14.22636pt\mathsf{let}\;\\{\ell,p\\}=v\;\mathsf{in}\;\mathsf{trans}[\mathsf{len}\;n\;\\{\ell,p\\}\;{=}(\beta)\;\mathsf{len}\;\ell\;{=}(p)\;n]\end{array}$

However, these definitions raise a question: why not simply write

(11) $\mathsf{Vec.len}\equiv\lambda\|n:\mathbb{N}\|,\lambda
v:\mathsf{Vec}\;A\;n,n$

The problem with the above definition is that $n$ is a ghost variable,
indicating we may use it in propositions and proofs but not generally in
terms. This is a critical distinction to be able to make: the specification of
a program may involve values which we do not want to manipulate at runtime.
For example, the correctness proof of a sorting routine might use an inductive
datatype of permutations, elements of which could potentially be much larger
than the list itself. By making a distinction between ghost and computational
variables, we can define an efficient erasure of refined terms (which contain
proofs) to simply-typed terms (which do not). For example, we can erase the
signature in equation 7 into a simple type:

(12) $\displaystyle|\forall
n:\mathbb{N},(v:\mathsf{Vec}\;A\;n)\to\\{x:\mathbb{N}\mid x=n\\}|$ (unfold,
erase quantified variable $n$)
$\displaystyle=\mathbf{1}\to|\\{\ell:\mathsf{List}\;A\mid\mathsf{len}\;\ell=n\\}\to\\{x:\mathbb{N}\mid
x=n\\}|$ (erasure distributes over function types)
$\displaystyle=\mathbf{1}\to|\\{\ell:\mathsf{List}\;A\mid\mathsf{len}\;\ell=n\\}|\to|\\{x:\mathbb{N}\mid
x=n\\}|$ (erase subset types to erased base types)
$\displaystyle=\mathbf{1}\to|\mathsf{List}\;A|\to|\mathbb{N}|$ (list erases to
list of erased type, $\mathbb{N}$ erases to $\mathbb{N}$)
$\displaystyle=\mathbf{1}\to\mathsf{List}\;|A|\to\mathbb{N}$

We can then erase the definition as follows:

(13) $\displaystyle|\lambda\|n:\mathbb{N}\|,\lambda
v:\mathsf{Vec}\;A\;n,\mathsf{let}\;\\{\ell,\\_\\}=v\;\mathsf{in}\;\mathsf{len}\;\ell|$
(unfold, erase quantified variable $n$) $\displaystyle=\lambda
n:\mathbf{1},|\lambda
v:\\{\ell:\mathsf{List}\;A\mid\mathsf{len}\;\ell=n\\},\mathsf{let}\;\\{\ell,\\_\\}=v\;\mathsf{in}\;\mathsf{len}\;\ell|$
(erasure distributes over binders) $\displaystyle=\lambda n:\mathbf{1},\lambda
v:|\\{\ell:\mathsf{List}\;A\mid\mathsf{len}\;\ell=n\\}|,|\mathsf{let}\;\\{\ell,\\_\\}=v\;\mathsf{in}\;\mathsf{len}\;\ell|$
(erase subset types to erased base types) $\displaystyle=\lambda
n:\mathbf{1},\lambda
v:|\mathsf{List}\;A|,|\mathsf{let}\;\\{\ell,\\_\\}=v\;\mathsf{in}\;\mathsf{len}\;\ell|$
(list erases to list of erased type) $\displaystyle=\lambda
n:\mathbf{1},\lambda
v:\mathsf{List}\;|A|,|\mathsf{let}\;\\{\ell,\\_\\}=v\;\mathsf{in}\;\mathsf{len}\;\ell|$
(erase distributes over $\mathsf{let}$) $\displaystyle=\lambda
n:\mathbf{1},\lambda
v:\mathsf{List}\;|A|,\mathsf{let}\;\ell=|v|\;\mathsf{in}\;|\mathsf{len}\;\ell|$
(variables erase to themselves) $\displaystyle=\lambda n:\mathbf{1},\lambda
v:\mathsf{List}\;|A|,\mathsf{let}\;\ell=v\;\mathsf{in}\;|\mathsf{len}\;\ell|$
(erasure distributes over application) $\displaystyle=\lambda
n:\mathbf{1},\lambda
v:\mathsf{List}\;|A|,\mathsf{let}\;\ell=v\;\mathsf{in}\;|\mathsf{len}|\;|\ell|$
(variables, $\mathsf{len}$ erase to themselves) $\displaystyle=\lambda
n:\mathbf{1},\lambda
v:\mathsf{List}\;|A|,\mathsf{let}\;\ell=v\;\mathsf{in}\;\mathsf{len}\;\ell:\mathbf{1}\to\mathsf{List}\;|A|\to\mathbb{N}$

At the type level, we erase any dependency information, leaving us with simple
types. Propositions are all either wholly erased or erased to the unit type.
At the term level, erasure essentially consists of recursively erasing ghost
variables and proofs into units and (in the case of proofs of falsehood) error
stops, yielding a well-typed term in the simply-typed lambda calculus extended
with an error stop effect (i.e., the exception monad). We will prove in
section 5 that the produced terms are always well-typed.

As expected, we see that erasure sends base types like $\mathbf{1}$ and
$\mathbb{N}$, as well as their literals like $()$ or $0$, to themselves.
Erasure distributes over (dependent) function types, i.e., $|(a:A)\to
B(a)|=|A|\to|B(a)|$, and correspondingly is recursively applied to the
argument type and result of a lambda function as follows: $|\lambda
a:A,b|=\lambda a:|A|,|b|$. Subset types are erased to the erasure of their
base type, i.e., we have $|\\{x:X\mid P(x)\\}|=|X|$. Erasure of the formation
and elimination rules for subset types is likewise as expected, with
$|\\{x,p\\}|=|x|$ and
$|\mathsf{let}\;\\{x,p\\}=e\;\mathsf{in}\;e^{\prime}|=\mathsf{let}\;x=|e|\;\mathsf{in}\;|e^{\prime}|$.
Similarly, universal quantifiers are erased to the unit type $\mathbf{1}$ as
follows: $|\forall a:A,B(a)|=\mathbf{1}\to|B(a)|$. Correspondingly, we erase
the introduction and elimination rules for intersection types like so:
$|\lambda\|a:A\|,b|=\lambda\\_:\mathbf{1},|b|$, $|f\;\|a\||=|f|\;()$. In
general, propositions and ghosts in value types (such as subsets) are erased
completely, whereas propositions and ghosts in function-style types (such as
intersection types) are erased to units to avoid problems with the eager
evaluation order of $\lambda_{\mathsf{stlc}}$. (See section 7 for a more
detailed discussion.)

Returning to the original question, erasing the definition in equation 11
yields the term $\lambda n:\mathbf{1},\lambda v:\mathsf{List}\;|A|,n$, which
is not well-typed at $\mathbf{1}\to\mathsf{List}\;|A|\to\mathbb{N}$. Another
way of thinking about this is that if $\mathsf{Vec.len}$ took the length $n$
as a computational argument, we would never need to call the function – we
would have to have the length in hand to call $\mathsf{Vec.len}$ in the first
place. However, in our setting, vectors are merely refined lists, which erase
into raw lists. A raw list does not carry its length $n$; but $n$ is a well-
defined property of its specification. Since the specification value $n$ gets
erased to a unit, then a program that wants to compute the length must
traverse the list – i.e., in equation 6 we call $\mathsf{List.len}$.

Another advantage of having explicit proofs as part of a refinement type
system is the ability to reuse previous theorems and perform proofs by
induction. For a simple example of this, consider the following definition of
addition for natural numbers:

(14) $n+m\equiv(\mathsf{natrec}\;n\;(\lambda
x,x)\;(\|\mathsf{succ}\;\\_\|,f\mapsto\lambda
x,\mathsf{succ}\;(f\;x)))\;m:\mathbb{N}$

$\mathsf{natrec}$ is the eliminator for the natural numbers, which is defined
essentially by iteration, with typing rule Natrec. The eliminator has the
standard behavior, given by reduction rules $\beta_{\mathsf{zero}}$ and
$\beta_{\mathsf{succ}}$, which essentially amount to substituting $z$ into $s$
recursively $n$ times. We can then use these axioms to prove that zero is a
left-identity by $\beta$-reduction, simply writing
$\mathsf{zero_{left}}:(\forall
n:\mathbb{N},0+n=n)\equiv\hat{\lambda}\|n:\mathbb{N}\|,\beta$. In contrast, we
need induction to prove that zero is a right-identity. To perform induction,
we introduce the $\mathsf{ind}$ eliminator for natural numbers, essentially
the propositional version of $\mathsf{natrec}$, with typing rule Ind. We may
then write

(15) $\displaystyle\begin{aligned} &\mathsf{zero_{right}}:(\forall
n:\mathbb{N},n+0=n)\equiv\\\ &\hskip
28.45274pt\hat{\lambda}\|n:\mathbb{N}\|,\mathsf{ind}[x\mapsto
x+0=x]\;n\;\beta\\\ &\hskip
72.2698pt(\mathsf{succ}\;n,u\mapsto\mathsf{trans}[(\mathsf{succ}\;n)+0\;{=}(\beta)\;\mathsf{succ}\;(n+0)\;{=}(u)\;\mathsf{succ}\;n]))&\end{aligned}$

Induction lets us prove many arithmetic facts without baking them into the
type system. For example, we can prove that addition is commutative as follows
(see figure 1 for helpers), where $\mathsf{symm}$ and $\mathsf{congr}$ are
proofs that equality is symmetric and transitive respectively:

(16) $\displaystyle\begin{aligned} &\mathsf{add_{comm}}:(\forall
n,m:\mathbb{N},n+m=m+n)\equiv\hat{\lambda}\|n:\mathbb{N}\|,\\\
&\quad\mathsf{ind}[x\mapsto\forall
m:\mathbb{N},x+m=m+x]\;n\;\mathsf{zero_{comm}}\\\
&\qquad(\mathsf{succ}\;n,u\mapsto\mathsf{trans}[\mathsf{succ}\;n+m\\\
&\qquad\quad\;{=}(\beta)\;\mathsf{succ}\;(n+m)\\\
&\qquad\quad\;{=}(\mathsf{congr}\;u)\;\mathsf{succ}\;(m+n)\\\
&\qquad\quad\;{=}(\beta)\;\mathsf{succ}\;m+n\\\
&\qquad\quad\;{=}(\mathsf{symm}\;(\mathsf{succ_{comm}\;\|m\|\;\|n\|}))\;m+\mathsf{succ}\;n])&\end{aligned}$

$\displaystyle\mathsf{zero_{comm}}:(\forall
n:\mathbb{N},0+n=n+0)\equiv\hat{\lambda}\|n:\mathbb{N}\|,\mathsf{trans}[0+n\;{=}(\beta)\;n\;{=}(\mathsf{zero_{right}}\;\|n\|)\;n+0]$
$\displaystyle\mathsf{succ_{right}}:(\forall
n,m:\mathbb{N},n+\mathsf{succ}\;m=\mathsf{succ}\;(n+m))\equiv$
$\displaystyle\qquad\hat{\lambda}\|n,m:\mathbb{N}\|,\mathsf{ind}[x\mapsto
x+(\mathsf{succ}\;m)=\mathsf{succ}\;(x+m)]\;n\;\beta$ $\displaystyle\hskip
56.9055pt\qquad(\mathsf{succ}\;n,u\mapsto\mathsf{trans}[\mathsf{succ}\;n+\mathsf{succ}\;m$
$\displaystyle\hskip
56.9055pt\qquad\quad\;{=}(\beta)\;\mathsf{succ}\;(n+\mathsf{succ}\;m)$
$\displaystyle\hskip
56.9055pt\qquad\quad\;{=}(u)\;\mathsf{succ}\;(\mathsf{succ}\;(n+m))$
$\displaystyle\hskip
56.9055pt\qquad\quad\;{=}(\beta)\;\mathsf{succ}\;(\mathsf{succ}\;n+m)]))$
$\displaystyle\mathsf{succ_{comm}}:(\forall
n:\mathbb{N},n+\mathsf{succ}\;m=\mathsf{succ}\;n+m)\equiv$
$\displaystyle\qquad\hat{\lambda}\|n:\mathbb{N}\|,\mathsf{trans}[n+\mathsf{succ}\;m\;{=}(\mathsf{succ_{right}}\;\|n\|\;\|m\|)\;\mathsf{succ}(n+m)\;{=}(\beta)\;\mathsf{succ}\;n+m]$

Figure 1. Helper definitions for equation 16

Helper definitions for equation 16

Note the ability to reuse theorems we have proved previously. Another
advantage of explicit proofs is that we do not need to encode even fundamental
facts into our core calculus since we can prove them from a small core of base
axioms. Minimizing the number of axioms simplifies the implementation of the
type-checker and reduces the size of the trusted codebase while allowing the
programmer to effectively write refinements and proofs using facts that the
language designer may not have considered.

##  4\. Formalization

We give $\lambda_{\mathsf{ert}}$’s grammar and typing rules in sections 4.1
and 4.2. We then give proofs of some expected metatheoretic properties, such
as substitution and regularity, in section 4.3.

###  4.1. Grammar

The grammar for $\lambda_{\mathsf{ert}}$ (given in figure 15(f) in the
appendix) consists of four separate syntactic categories: types $A$,
propositions $\varphi$, terms $a$, and proofs $p$. We denote the set of
(syntactically) well-formed terms living in each by $\mathsf{Type}$,
$\mathsf{Prop}$, $\mathsf{Term}$, and $\mathsf{Proof}$, respectively. We may
then define a typing context $\Gamma$ as a list of computational variables
$x:A$, ghost variables $\|x:A\|$, and propositional variables $u:\varphi$, as
in figure 3.

Ghost variables only appear within proofs, types, and propositions, whereas
computational variables can occur anywhere, including both computational and
logical terms. Typing contexts are telescopic, so types and propositions
appearing later in the context may depend on previously defined variables. We
use these syntactic categories to state the shape of
$\lambda_{\mathsf{ert}}$’s typing judgments in figure 2.

Judgment | Meaning
---|---
$\Gamma\;\mathsf{ok}$ |  $\Gamma$ is a well-formed context
$\Gamma\vdash A\;\mathsf{ty}$ |  $A$ is a well-formed type in $\Gamma$
$\Gamma\vdash\varphi\;\mathsf{pr}$ |  $\varphi$ is a well-formed proposition in $\Gamma$
$\Gamma\vdash a:A$ |  $a$ may consistently be assigned type $A$ in $\Gamma$
$\Gamma\vdash p:\varphi$ |  $p$ is a proof of $\varphi$ in $\Gamma$

Figure 2. $\lambda_{\mathsf{ert}}$ typing judgements

$\lambda_{\mathsf{ert}}$ typing judgements

A context is _well-formed_ if the types of each of its variables are well-
formed in the context made up of all previously defined variables, with the
context well-formedness rules in figure 3.

$\prftree{\cdot\;\mathsf{ok}}\qquad\prftree{\Gamma\;\mathsf{ok}}{\Gamma\vdash
A\;\mathsf{ty}}{\Gamma,x:A\;\mathsf{ok}}\qquad\prftree{\Gamma\;\mathsf{ok}}{\Gamma\vdash
A\;\mathsf{ty}}{\Gamma,\|x:A\|\;\mathsf{ok}}\qquad\prftree{\Gamma\;\mathsf{ok}}{\Gamma\vdash\varphi\;\mathsf{pr}}{\Gamma,u:\varphi\;\mathsf{ok}}$

Figure 3. $\lambda_{\mathsf{ert}}$ context well-formedness rules

ERT context well-formedness rules

The presence of both computational and ghost variables means that our contexts
have additional structural properties beyond the usual ones such as weakening
and exchange. Since a computational variable can be used in more places than a
ghost variable, we introduce the concept of an _upgrade_. When we upgrade a
context, some of the ghost variables can be replaced by computational
variables with the same name and type. So, for example, the context
$\|x:A\|,y:B$ can be upgraded to $x:A,y:B$. In figure 4, we formalise this
with the rules of the judgment ${\Delta}\leq{\Gamma}$, which reads ”$\Delta$
upgrades $\Gamma$”.

$\prftree{{\Delta}\leq{\Gamma}}{{\Delta,x:A}\leq{\Gamma,\|x:A\|}}\qquad\prftree{{\Delta}\leq{\Gamma}}{{\Delta,H}\leq{\Gamma,H}}\qquad\prftree{}{{\cdot}\leq{\cdot}}$

Figure 4. $\lambda_{\mathsf{ert}}$ context upgrade rules, where $H$ ranges
over hypotheses $x:A$, $\|x:A\|$, $p:\varphi$

ERT context upgrade rules, where H ranges over hypotheses

We now define the _upgrade_ of $\Gamma$, written ${\Gamma}^{\uparrow}$, to be
the context with all ghost variables in $\Gamma$ replaced by term variables,
that is,

(17)
${\cdot}^{\uparrow}=\cdot\qquad{(\Gamma,\|x:A\|)}^{\uparrow}={\Gamma}^{\uparrow},x:A,\qquad{(\Gamma,x:A)}^{\uparrow}={\Gamma}^{\uparrow},x:A,\qquad{(\Gamma,u:\varphi)}^{\uparrow}={\Gamma}^{\uparrow},u:\varphi$

Note that ${{\Gamma}^{\uparrow}}\leq{\Gamma}$ (but
${\Gamma}\leq{{\Gamma}^{\uparrow}}$ iff $\Gamma$ contains no ghost variables).
A context $\Delta$ which upgrades $\Gamma$ types more terms than $\Gamma$,
since we may use a computational variable anywhere a ghost variable is
expected, but not vice versa. In particular, we may prove the following lemma:

###### Lemma 4.1 (Upgrade).

Given contexts ${\Delta}\leq{\Gamma}$,

  * •

If $\Gamma\vdash\varphi\;\mathsf{pr}$, then
$\Delta\vdash\varphi\;\mathsf{pr}$. In particular, if
$\Gamma\vdash\varphi\;\mathsf{pr}$, then
${\Gamma}^{\uparrow}\vdash\varphi\;\mathsf{pr}$.

  * •

If $\Gamma\vdash A\;\mathsf{ty}$, then $\Delta\vdash A\;\mathsf{ty}$. In
particular, if $\Gamma\vdash\varphi\;\mathsf{ty}$, then
${\Gamma}^{\uparrow}\vdash\varphi\;\mathsf{ty}$.

  * •

If $\Gamma\vdash p:\varphi$, then $\Delta\vdash p:\varphi$. In particular, if
$\Gamma\vdash p:\varphi$, then ${\Gamma}^{\uparrow}\vdash p:\varphi$.

  * •

If $\Gamma\vdash a:A$, then $\Delta\vdash a:A$. In particular, if
$\Gamma\vdash a:A$, then ${\Gamma}^{\uparrow}\vdash a:A$.

  * •

If $\Gamma\;\mathsf{ok}$, then $\Delta\;\mathsf{ok}$. In particular, if
$\Gamma\;\mathsf{ok}$, then ${\Gamma}^{\uparrow}\;\mathsf{ok}$.

Since the only difference between computational and ghost variables is that
ghosts can’t be used in computational terms, this distinction does not matter
for proofs, or for proposition- and type-well-formedness. Formally:

###### Lemma 4.2 (Downgrade).

Given contexts ${\Delta}\leq{\Gamma}$,

  * •

If $\Delta\vdash\varphi\;\mathsf{pr}$, then
$\Gamma\vdash\varphi\;\mathsf{pr}$. In particular, if
${\Gamma}^{\uparrow}\vdash\varphi\;\mathsf{pr}$, then
$\Gamma\vdash\varphi\;\mathsf{pr}$.

  * •

If $\Delta\vdash A\;\mathsf{ty}$, then $\Gamma\vdash A\;\mathsf{ty}$. In
particular, if ${\Gamma}^{\uparrow}\vdash\varphi\;\mathsf{ty}$, then
$\Gamma\vdash\varphi\;\mathsf{ty}$.

  * •

If $\Delta\vdash p:\varphi$, then $\Gamma\vdash p:\varphi$. In particular, if
${\Gamma}^{\uparrow}\vdash p:\varphi$, then $\Gamma\vdash p:\varphi$.

  * •

If $\Delta\;\mathsf{ok}$, then $\Gamma\;\mathsf{ok}$. In particular, if
${\Gamma}^{\uparrow}\;\mathsf{ok}$, then $\Gamma\;\mathsf{ok}$.

###  4.2. Typing Rules

The type formation rules for $\lambda_{\mathsf{ert}}$ are collected in figure
5, the term formation rules in figure 7, the proposition formation rules in
figure 6, and the proof rules and axioms in figures 8 and 9 respectively.

####  4.2.1. Equality

The heart of the $\lambda_{\mathsf{ert}}$ type refinement system is the
equality proposition $a=_{A}b$, which is verified by proofs that $a=b$ where
$a$ and $b$ are interpreted as elements of the type $A$. This has formation
rule Eq-WF, which checks that $a$ and $b$ are well-typed in an upgraded
context. Because equality is a mathematical proposition, we may use ghost
variables freely. Furthermore, note that we can consider equalities between
terms of any type, including terms of higher type such as function types. This
has often been challenging to support with refinement types (see Vazou and
Greenberg (2022) for a detailed discussion), but is unproblematic with
$\lambda_{\mathsf{ert}}$.

$\displaystyle\prftree[r]{{\scriptsize\textsf{Fn-WF}}}{\Gamma\vdash
A\;\mathsf{ty}}{\Gamma,x:A\vdash B\;\mathsf{ty}}{\Gamma\vdash(x:A)\to
B\;\mathsf{ty}}\qquad\prftree[r]{{\scriptsize\textsf{Pair-WF}}}{\Gamma\vdash
A\;\mathsf{ty}}{\Gamma,x:A\vdash B\;\mathsf{ty}}{\Gamma\vdash(x:A)\times
B\;\mathsf{ty}}$ $\displaystyle\prftree[r]{{\scriptsize\textsf{Intr-
WF}}}{\Gamma\vdash A\;\mathsf{ty}}{\Gamma,x:A\vdash
B\;\mathsf{ty}}{\Gamma\vdash\forall
x:A,B\;\mathsf{ty}}\qquad\prftree[r]{{\scriptsize\textsf{Union-
WF}}}{\Gamma\vdash A\;\mathsf{ty}}{\Gamma,x:A\vdash
B\;\mathsf{ty}}{\Gamma\vdash\exists x:A,B\;\mathsf{ty}}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Pre-
WF}}}{\Gamma\vdash\varphi\;\mathsf{pr}}{\Gamma,u:\varphi\vdash
A\;\mathsf{ty}}{\Gamma\vdash({u}:{\varphi})\Rightarrow{A}\;\mathsf{ty}}\qquad\prftree[r]{{\scriptsize\textsf{Set-
WF}}}{\Gamma\vdash
A\;\mathsf{ty}}{\Gamma,x:A\vdash\varphi\;\mathsf{pr}}{\Gamma\vdash\\{x:A\mid\varphi\\}\;\mathsf{ty}}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Unit-
WF}}}{}{\Gamma\vdash\mathbf{1}\;\mathsf{ty}}\qquad\prftree[r]{{\scriptsize\textsf{Coprod-
WF}}}{\Gamma\vdash A\;\mathsf{ty}}{\Gamma\vdash B\;\mathsf{ty}}{\Gamma\vdash
A+B\;\mathsf{ty}}\qquad\prftree[r]{{\scriptsize\textsf{Nats-
WF}}}{}{\Gamma\vdash\mathbb{N}\;\mathsf{ty}}$

Figure 5. $\lambda_{\mathsf{ert}}$ Type Well-formedness

$\lambda_{\mathsf{ert}}$ Type Well-formedness

$\displaystyle\prftree[r]{{\scriptsize\textsf{Imp-
WF}}}{\Gamma\vdash\varphi\;\mathsf{pr}}{\Gamma,u:\varphi\vdash\psi\;\mathsf{pr}}{\Gamma\vdash({u}:{\varphi})\Rightarrow{\psi}\;\mathsf{pr}}\quad\prftree[r]{{\scriptsize\textsf{Or-
WF}}}{\Gamma\vdash\varphi\;\mathsf{pr}}{\Gamma\vdash\psi\;\mathsf{pr}}{\Gamma\vdash\varphi\lor\psi\;\mathsf{pr}}\quad\prftree[r]{{\scriptsize\textsf{And-
WF}}}{\Gamma\vdash\varphi\;\mathsf{pr}}{\Gamma,u:\varphi\vdash\psi\;\mathsf{pr}}{\Gamma\vdash(u:\varphi)\land\psi\;\mathsf{pr}}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Univ-WF}}}{\Gamma\vdash
A\;\mathsf{ty}}{\Gamma,x:A\vdash\varphi\;\mathsf{pr}}{\Gamma\vdash\forall
x:A,\varphi\;\mathsf{pr}}\qquad\prftree[r]{{\scriptsize\textsf{Exists-
WF}}}{\Gamma\vdash
A\;\mathsf{ty}}{\Gamma,x:A\vdash\varphi\;\mathsf{pr}}{\Gamma\vdash\exists
x:A,\varphi\;\mathsf{pr}}$ $\displaystyle\prftree[r]{{\scriptsize\textsf{Eq-
WF}}}{\Gamma\vdash A\;\mathsf{ty}}{{\Gamma}^{\uparrow}\vdash
a:A}{{\Gamma}^{\uparrow}\vdash b:A}{\Gamma\vdash
a=_{A}b\;\mathsf{pr}}\qquad\prftree[r]{{\scriptsize\textsf{True-
WF}}}{}{\Gamma\vdash\top\;\mathsf{pr}}\qquad\prftree[r]{{\scriptsize\textsf{False-
WF}}}{}{\Gamma\vdash\bot\;\mathsf{pr}}$

Figure 6. $\lambda_{\mathsf{ert}}$ Proposition Well-formedness

$\lambda_{\mathsf{ert}}$ Proposition Well-formedness

$\displaystyle\prftree[r]{{\scriptsize\textsf{Var}}}{}{\Gamma,x:A\vdash
x:A}\qquad\prftree[r]{{\scriptsize\textsf{Absurd}}}{\Gamma\vdash
p:\bot}{\Gamma\vdash\mathsf{absurd}\;p:A}\qquad\prftree[r]{{\scriptsize\textsf{Zero}}}{\Gamma\vdash
0:\mathbb{N}}\qquad\prftree[r]{{\scriptsize\textsf{Succ}}}{\Gamma\vdash\mathsf{succ}:\mathbb{N}\to\mathbb{N}}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Unit}}}{\Gamma\vdash():\mathbf{1}}\qquad\prftree[r]{{\scriptsize\textsf{Lam}}}{\Gamma,x:A\vdash
e:B}{\Gamma\vdash\lambda x:A,e:(x:A)\to
B}\qquad\prftree[r]{{\scriptsize\textsf{App}}}{\Gamma\vdash l:(x:A)\to
B}{\Gamma\vdash r:A}{\Gamma\vdash l\;r:[r/x]B}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Pair}}}{\Gamma\vdash
l:A}{\Gamma\vdash r:[l/x]B}{\Gamma\vdash(l,r):(x:A)\times
B}\qquad\prftree[r]{{\scriptsize\textsf{Inl}}}{\Gamma\vdash
e:A}{\Gamma\vdash\mathsf{inl}\;e:A+B}\qquad\prftree[r]{{\scriptsize\textsf{Inr}}}{\Gamma\vdash
e:B}{\Gamma\vdash\mathsf{inr}\;e:A+B}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Let-Pair}}}{\Gamma\vdash
e:(x:A)\times B}{\Gamma,z:(x:A)\times B\vdash
C\;\mathsf{ty}}{\Gamma,x:A,y:B\vdash
e^{\prime}:[(x,y)/z]C}{\Gamma\vdash\mathsf{let}\;(x,y):(x:A)\times
B=e\;\mathsf{in}\;e^{\prime}:[e/z]C}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Cases}}}{\Gamma,x:A+B\vdash
C\;\mathsf{ty}}{\Gamma\vdash e:A+B}{\Gamma,y:A\vdash
l:[\mathsf{inl}\;y/x]C}{\Gamma,z:B\vdash
r:[\mathsf{inr}\;z/x]C}{\Gamma\vdash\mathsf{cases}\;[x\mapsto
C]\;e\;(\mathsf{inl}\;y\mapsto l)\;(\mathsf{inr}\;z\mapsto r):[e/x]C}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Lam-Pr}}}{\Gamma,u:\varphi\vdash
e:A}{\Gamma\vdash\lambda
u:\varphi.e:({u}:{\varphi})\Rightarrow{A}}\qquad\prftree[r]{{\scriptsize\textsf{App-
Pr}}}{\Gamma\vdash f:({u}:{\varphi})\Rightarrow{A}}{\Gamma\vdash
p:\varphi}{\Gamma\vdash f\;p:[p/x]A}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Set}}}{\Gamma\vdash
a:A}{\Gamma\vdash
p:[a/x]\varphi}{\Gamma\vdash\\{a,p\\}:\left\\{{x}:{A}\mid{\varphi}\right\\}}\qquad\prftree[r]{{\scriptsize\textsf{Pair-
Ir}}}{{\Gamma}^{\uparrow}\vdash a:A}{\Gamma\vdash
b:[a/x]B}{\Gamma\vdash(\|a\|,b):\exists a:A,B}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Let-Set}}}{\Gamma\vdash
e:\left\\{{x}:{A}\mid{\varphi}\right\\}}{\Gamma,z:\left\\{{x}:{A}\mid{\varphi}\right\\}\vdash
C\;\mathsf{ty}}{\Gamma,x:A,u:\varphi\vdash
e^{\prime}:[\\{x,u\\}/z]C}{\Gamma\vdash\mathsf{let}\;\\{x,u\\}:\left\\{{x}:{A}\mid{\varphi}\right\\}=e\;\mathsf{in}\;e^{\prime}:[e/z]C}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Lam-Ir}}}{\Gamma,\|x:A\|\vdash
e:B}{\Gamma\vdash\lambda\|x:A\|,e:\forall
x:A,B}\qquad\prftree[r]{{\scriptsize\textsf{App-Ir}}}{\Gamma\vdash f:\forall
x:A,B}{{\Gamma}^{\uparrow}\vdash a:A}{\Gamma\vdash f\|a\|:[a/x]B}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Let-Ir}}}{\Gamma\vdash e:\exists
x:A,B}{\Gamma,z:\exists x:A,B\vdash C\;\mathsf{ty}}{\Gamma,\|x:A\|,y:B\vdash
e^{\prime}:[(\|x\|,y)/z]C}{\Gamma\vdash\mathsf{let}\;(\|x\|,y):\exists
x:A,B=e\;\mathsf{in}\;e^{\prime}:[e/z]C}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Natrec}}}{\Gamma,n:\mathbb{N}\vdash
C\;\mathsf{ty}}{\Gamma\vdash e:\mathbb{N}}{\Gamma\vdash
z:[0/n]C}{\Gamma,\|n:\mathbb{N}\|,y:C\vdash
s:[\mathsf{succ}\;n/n]C}{\Gamma\vdash\mathsf{natrec}[n\mapsto
C]\;e\;z\;(\|\mathsf{succ}\;x\|,y\mapsto s):[e/n]C}$

Figure 7. $\lambda_{\mathsf{ert}}$ Term Typing

$\lambda_{\mathsf{ert}}$ Term Typing

$\displaystyle\prftree[r]{{\scriptsize\textsf{Var-
Pr}}}{}{\Gamma,u:\varphi\vdash
u:\varphi}\qquad\prftree[r]{{\scriptsize\textsf{True}}}{\Gamma\vdash\langle\rangle:\top}\qquad\prftree[r]{{\scriptsize\textsf{Absurd-
Pr}}}{\Gamma\vdash p:\bot}{\Gamma\vdash\mathsf{absurd}\;p:\varphi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Imp}}}{\Gamma,u:\varphi\vdash
p:\psi}{\Gamma\vdash\hat{\lambda}u:\varphi,p:({u}:{\varphi})\Rightarrow{\psi}}\qquad\prftree[r]{{\scriptsize\textsf{MP}}}{\Gamma\vdash
p:({u}:{\varphi})\Rightarrow{\psi}}{\Gamma\vdash q:\psi}{\Gamma\vdash
p\;q:[q/u]B}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{And}}}{\Gamma\vdash
p:\varphi}{\Gamma\vdash q:[p/u]\psi}{\Gamma\vdash\langle
p,q\rangle:(u:\varphi)\land\psi}\qquad\prftree[r]{{\scriptsize\textsf{Orl}}}{\Gamma\vdash
p:\varphi}{\Gamma\vdash\mathsf{orl}\;p:\varphi\lor\psi}\qquad\prftree[r]{{\scriptsize\textsf{Orr}}}{\Gamma\vdash
p:\psi}{\Gamma\vdash\mathsf{orr}\;p:\varphi\lor\psi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Let-And}}}{\Gamma\vdash
p:(u:\varphi)\land\psi}{\Gamma,w:(u:\varphi)\land\psi\vdash\theta\;\mathsf{pr}}{\Gamma,u:\varphi,v:\psi\vdash
q:[\langle u,v\rangle/w]\theta}{\Gamma\vdash\mathsf{let}\;\langle
u,v\rangle:(u:\varphi)\land\psi=p\;\mathsf{in}\;q:[p/w]\theta}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Cases-
Or}}}{\Gamma,u:\varphi\lor\psi\vdash\theta\;\mathsf{pr}}{\Gamma\vdash
p:\varphi\lor\psi}{\Gamma,v:\varphi\vdash
l:[\mathsf{orl}\;v/u]\theta}{\Gamma,w:\psi\vdash
r:[\mathsf{orr}\;w/u]\theta}{\Gamma\vdash\mathsf{cases}_{\mathsf{or}}\;[u\mapsto\theta]\;p\;(\mathsf{orl}\;v\mapsto
l)\;(\mathsf{orr}\;w\mapsto r):[e/u]C}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Gen}}}{\Gamma,\|x:A\|\vdash
p:\varphi}{\Gamma\vdash\hat{\lambda}\|x:A\|,p:\forall
x:A,\varphi}\qquad\prftree[r]{{\scriptsize\textsf{Spec}}}{\Gamma\vdash
p:\forall x:A,\varphi}{{\Gamma}^{\uparrow}\vdash a:A}{\Gamma\vdash
p\;\|a\|:[a/x]\varphi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Wit}}}{{\Gamma}^{\uparrow}\vdash
a:A}{\Gamma\vdash p:[a/x]\varphi}{\Gamma\vdash\langle\|a\|,p\rangle:\exists
x:A,\varphi}$ $\displaystyle\prftree[r]{{\scriptsize\textsf{Let-
Exists}}}{\Gamma\vdash p:\exists x:A,\varphi}{\Gamma,v:\exists
x:A,\varphi\vdash\psi\;\mathsf{pr}}{\Gamma,x:A,u:\varphi\vdash
q:[\langle\|a\|,p\rangle/v]\psi}{\Gamma\vdash\mathsf{let}\;\langle\|x\|,u\rangle:\exists
x:A,\varphi=p\;\mathsf{in}\;q:[p/v]\psi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Let-Pair-
Pr}}}{{\Gamma}^{\uparrow}\vdash e:(x:A)\times B}{\Gamma,z:(x:A)\times
B\vdash\varphi\;\mathsf{pr}}{\Gamma,x:A,y:B\vdash
e^{\prime}:[(x,y)/z]\varphi}{\Gamma\vdash\mathsf{let}\;(x,y):(x:A)\times
B=e\;\mathsf{in}\;e^{\prime}:[e/z]\varphi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Let-Set-
Pr}}}{{\Gamma}^{\uparrow}\vdash
e:\left\\{{x}:{A}\mid{\varphi}\right\\}}{\Gamma,z:\left\\{{x}:{A}\mid{\varphi}\right\\}\vdash\psi\;\mathsf{pr}}{\Gamma,x:A,u:\varphi\vdash
e^{\prime}:[\\{x,y\\}/z]\psi}{\Gamma\vdash\mathsf{let}\;\\{x,u\\}:\left\\{{x}:{A}\mid{\varphi}\right\\}=e\;\mathsf{in}\;e^{\prime}:[e/z]\psi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Let-Ir-
Pr}}}{{\Gamma}^{\uparrow}\vdash e:\exists x:A,\varphi}{\Gamma,z:\exists
x:A,B\vdash\varphi\;\mathsf{ty}}{\Gamma,x:A,y:B\vdash
e^{\prime}:[(\|x|\|,y)/z]\varphi}{\Gamma\vdash\mathsf{let}\;(\|x\|,y):\exists
x:A,B=e\;\mathsf{in}\;e^{\prime}:[e/z]\varphi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Subst}}}{{\Gamma}^{\uparrow}\vdash
a:A}{{\Gamma}^{\uparrow}\vdash b:A}{\Gamma\vdash p:a=_{A}b}{\Gamma\vdash
q:[a/x]\varphi}{\Gamma\vdash\mathsf{subst}[x\mapsto\varphi][a][b]\;p\;q:[b/x]\varphi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Cases-
Pr}}}{\Gamma,x:A+B\vdash\varphi;\mathsf{pr}}{\Gamma\vdash
e:A+B}{\Gamma,y:A\vdash l:[\mathsf{inl}\;y/x]\varphi}{\Gamma,z:B\vdash
r:[\mathsf{inr}\;z/x]\varphi}{\Gamma\vdash\mathsf{cases}\;[x\mapsto\varphi]\;e\;(\mathsf{inl}\;y\mapsto
l)\;(\mathsf{inr}\;z\mapsto r):[e/x]\varphi}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Ind}}}{\Gamma,n:\mathbb{N}\vdash\varphi\;\mathsf{pr}}{{\Gamma}^{\uparrow}\vdash
e:\mathbb{N}}{\Gamma\vdash
z:[0/n]\varphi}{\Gamma,n:\mathbb{N},y:\varphi:s:[\mathsf{succ}\;n/n]\varphi}{\Gamma\vdash\mathsf{ind}[n\mapsto\varphi]\;e\;z\;(\mathsf{succ}\;n,y\mapsto
s):[e/n]\varphi}$

Figure 8. $\lambda_{\mathsf{ert}}$ Proof Typing

$\lambda_{\mathsf{ert}}$ Proof Typing

$\displaystyle\prftree[r]{{\scriptsize\textsf{Rfl}}}{{\Gamma}^{\uparrow}\vdash
a:A}{\Gamma\vdash\mathsf{rfl}\;a:a=_{A}a}\qquad\prftree[r]{{\scriptsize\textsf{Uniq}}}{{\Gamma}^{\uparrow}\vdash
a:\mathbf{1}}{\Gamma\vdash\mathsf{uniq}\;a:a=_{\mathbf{1}}()}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{Discr}}}{{\Gamma}^{\uparrow}\vdash
a:A}{{\Gamma}^{\uparrow}\vdash b:B}{\Gamma\vdash
p:\mathsf{inl}\;a=_{A+B}\mathsf{inr}\;b}{\Gamma\vdash\mathsf{discr}\;a\;b\;p:\bot}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{pr}}$}}}{{\Gamma}^{\uparrow},u:\varphi\vdash
e:A}{\Gamma\vdash p:\varphi}{\Gamma\vdash\beta_{\mathsf{pr}}(u\mapsto
e)\;p:(\hat{\lambda}u:\varphi.e)\;p=_{[p/u]A}[p/u]e}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{ty}}$}}}{{\Gamma}^{\uparrow},x:A\vdash
e:B}{{\Gamma}^{\uparrow}\vdash a:A}{\Gamma\vdash\beta_{\mathsf{ty}}(x\mapsto
e)\;a:(\lambda x:A.e)\;a=_{[a/x]B}[a/x]e}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{ir}}$}}}{{\Gamma}^{\uparrow},x:A\vdash
e:B}{{\Gamma}^{\uparrow}\vdash a:A}{\Gamma\vdash\beta_{\mathsf{ir}}(x\mapsto
e)\;a:(\lambda\|x:A\|.e)\;\|a\|=_{[a/x]B}[a/x]e}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{left}}$}}}{{\Gamma}^{\uparrow}\vdash
a:A}{{\Gamma}^{\uparrow},y:A\vdash
l:[\mathsf{inl}\;y/x]C}{{\Gamma}^{\uparrow},z:B\vdash
r:[\mathsf{inr}\;z/x]C}{\begin{array}[]{rl}\Gamma\vdash&\beta_{\mathsf{left}}[x\mapsto
C]\;(\mathsf{inl}\;y\mapsto l)\;(\mathsf{inr}\;z\mapsto
r)\;(\mathsf{inl}\;a)\\\ :&\mathsf{cases}[x\mapsto
C]\;(\mathsf{inl}\;a)\;(\mathsf{inl}\;y\mapsto l)\;(\mathsf{inr}\;z\mapsto
r)=_{[\mathsf{inl}\;a/x]C}[a/y]l\end{array}}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{right}}$}}}{{\Gamma}^{\uparrow}\vdash
b:B}{{\Gamma}^{\uparrow},y:A\vdash
l:[\mathsf{inl}\;y/x]C}{{\Gamma}^{\uparrow},z:B\vdash
r:[\mathsf{inr}\;z/x]C}{\begin{array}[]{rl}\Gamma\vdash&\beta_{\mathsf{right}}[x\mapsto
C]\;(\mathsf{inl}\;y\mapsto l)\;(\mathsf{inr}\;z\mapsto
r)\;(\mathsf{inr}\;b)\\\ :&\mathsf{cases}[x\mapsto
C]\;(\mathsf{inr}\;b)\;(\mathsf{inl}\;y\mapsto l)\;(\mathsf{inr}\;z\mapsto
r)=_{[\mathsf{inr}\;b/x]C}[b/z]r\end{array}}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{zero}}$}}}{{\Gamma}^{\uparrow}\vdash
z:[0/x]C}{{\Gamma}^{\uparrow},x:\mathbb{N},y:C\vdash
s:[\mathsf{succ}\;x/x]C}{\Gamma\vdash\beta_{\mathsf{zero}}[x\mapsto
C]\;z\;(\|\mathsf{succ}\;x\|,y\mapsto s):\mathsf{natrec}[x\mapsto
C]\;0\;z\;(\|\mathsf{succ}\;x\|,y\mapsto s)=_{[0/x]C}z}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{succ}}$}}}{{\Gamma}^{\uparrow}\vdash
e:\mathbb{N}}{{\Gamma}^{\uparrow}\vdash
z:[0/x]C}{{\Gamma}^{\uparrow},x:\mathbb{N},y:C\vdash
s:[\mathsf{succ}\;x/x]C}{\begin{array}[]{rl}\Gamma\vdash&\beta_{\mathsf{succ}}[x\mapsto
C]\;(\mathsf{succ}\;e)\;z\;(\|\mathsf{succ}\;x\|,y\mapsto s)\\\
:&\mathsf{natrec}[x\mapsto
C]\;(\mathsf{succ}\;e)\;z\;(\|\mathsf{succ}\;x\|,y\mapsto s)\\\
&=_{[\mathsf{succ}\;e/x]C}[(\mathsf{natrec}[x\mapsto
C]\;e\;z\;(\|\mathsf{succ}\;x\|,y\mapsto s))/y][e/x]s\end{array}}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{pair}}$}}}{{\Gamma}^{\uparrow}\vdash
a:A}{{\Gamma}^{\uparrow}\vdash b:[a/y]B}{{\Gamma}^{\uparrow},y:A,z:B\vdash
e:[(y,z)/x]C}{\Gamma\vdash\beta_{\mathsf{pair}}\;(a,b)\;((y,z)\mapsto
e):(\mathsf{let}\;(y,z)=(a,b)\;\mathsf{in}\;e)=_{[(a,b)/x]C}[b/z][a/y]e}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{set}}$}}}{{\Gamma}^{\uparrow}\vdash
a:A}{{\Gamma}^{\uparrow}\vdash
p:[a/y]\varphi}{{\Gamma}^{\uparrow},y:A,u:\varphi\vdash
e:[\\{y,u\\}/x]C}{\Gamma\vdash\beta_{\mathsf{set}}\;\\{a,p\\}\;((y,u)\mapsto
e):(\mathsf{let}\;\\{y,u\\}=\\{a,p\\}\;\mathsf{in}\;e)=_{[\\{a,p\\}/x]C}[p/u][a/y]e}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\beta_{\mathsf{repr}}$}}}{{\Gamma}^{\uparrow}\vdash
a:A}{{\Gamma}^{\uparrow}\vdash b:[a/y]B}{{\Gamma}^{\uparrow},y:A,z:B\vdash
e:[(\|y\|,z)/x]C}{\Gamma\vdash\beta_{\mathsf{repr}}\;(\|a\|,b)\;((y,z)\mapsto
e):(\mathsf{let}\;(\|y\|,z)=(\|a\|,b)\;\mathsf{in}\;e)=_{[(\|a\|,b)/x]C}[b/z][a/y]e}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\eta_{\mathsf{ty}}$}}}{{\Gamma}^{\uparrow}\vdash
f:(x:A)\to B}{\Gamma\vdash\eta_{\mathsf{ty}}\;f:\lambda x:A,f\;x=_{(x:A)\to
B}f}\qquad\prftree[r]{{\scriptsize\textsf{Ir-Pr}}}{\Gamma\vdash
A\;\mathsf{ty}}{{\Gamma}^{\uparrow},u:\varphi\vdash
e:A}{{\Gamma}^{\uparrow}\vdash p:\varphi}{{\Gamma}^{\uparrow}\vdash
q:\varphi}{\Gamma\vdash\mathsf{ir}_{\mathsf{pr}}[u\mapsto
e]\;p\;q:[p/u]e=_{A}[q/u]e}$ $\displaystyle\prftree[r]{{\scriptsize\textsf{Ir-
Ty}}}{\Gamma\vdash B\;\mathsf{ty}}{{\Gamma}^{\uparrow}\vdash e:\forall
x:A,B}{{\Gamma}^{\uparrow}\vdash a:A}{{\Gamma}^{\uparrow}\vdash
b:A}{\Gamma\vdash\mathsf{ir}_{\mathsf{ty}}\;e\;a\;b:e\;\|a\|=_{B}e\;\|b\|}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\eta_{\mathsf{ir}}$}}}{{\Gamma}^{\uparrow}\vdash
f:\forall x:A,B}{{\Gamma}^{\uparrow}\vdash g:\forall
x:A,B}{{\Gamma}^{\uparrow}\vdash i:A}{\Gamma,x:A\vdash
p:f\;\|x\|=_{B}g\;\|x\|}{\Gamma\vdash\eta_{\mathsf{ir}}\;f\;g\;i\;p:f=_{\forall
x:A,B}g}$
$\displaystyle\prftree[r]{{\scriptsize\textsf{$\eta_{\mathsf{pr}}$}}}{{\Gamma}^{\uparrow}\vdash
f:({x}:{\varphi})\Rightarrow{B}}{{\Gamma}^{\uparrow}\vdash
g:({x}:{\varphi})\Rightarrow{B}}{{\Gamma}^{\uparrow}\vdash
i:\varphi}{\Gamma,x:\varphi\vdash
p:f\;x=_{B}g\;x}{\Gamma\vdash\eta_{\mathsf{pr}}\;f\;g\;i\;p:f=_{({x}:{\varphi})\Rightarrow{B}}g}$

Figure 9. $\lambda_{\mathsf{ert}}$ Axiom Typing

$\lambda_{\mathsf{ert}}$ Axiom Typing

The introduction rule is the standard reflexivity axiom, Rfl, and equalities
may be eliminated via substitution using the rule Subst. The substitution
eliminator is powerful enough to prove the other equality axioms, such as, for
example, transitivity:

(18) $\prftree{\Gamma\vdash p:a=_{A}b}{\Gamma\vdash
q:b=_{A}c}{\mathsf{trans}\;p\;q\equiv\mathsf{subst}[x\mapsto
a=_{A}x][b][c]\;q\;p:a=_{A}c}$

Type equality $\lambda_{\mathsf{ert}}$ is just $\alpha$-equivalence, and so
any equations which would have come via judgemental equality in a dependent
type theory must be expressed as equality axioms. For example, beta-reduction
for functions is expressed via the axiom $\beta_{\mathsf{ty}}$, and there are
similar rules for each of the type constructors in the language. Furthermore,
because proofs are computationally irrelevant, they support an extensionality
principle: the axiom Ir-Pr lets us replace any proof $p$ with any other proof
$q$.

####  4.2.2. Type Structure

$\lambda_{\mathsf{ert}}$ has (refinements of) the usual type constructors of
the simply-typed lambda calculus, such as functions, pairs, sum types, and
datatypes like natural numbers, as well as type constructors specific to
refinement types such as subset types, generalised intersections and unions,
and preconditions.

Dependent functions of type $(x:A)\to B$ may be introduced by lambda
abstraction, via the rule Lam, and may be eliminated by application, via the
rule App. The corresponding $\beta$ and $\eta$ equations are introduced
axiomatically, with the rules $\beta_{\mathsf{ty}}$ and $\eta_{\mathsf{ty}}$.
Each of the $\beta$ and $\eta$ axioms is subscripted with an annotation naming
the type former it is for. For example, the subscript ”$\mathsf{ty}$” in
$\beta_{\mathsf{ty}}$ refers to the fact that dependent function types are
parameterized by a term variable (with a type). The rule application itself is
annotated with the function body and argument.

While dependent function types abstract over a _computational_ variable, we
can also abstract over _ghost_ or _(computationally) irrelevant_ variables,
yielding a form of _intersection type_. The type well-formedness conditions
for $\forall x:A,B$ (in Intr-WF) are essentially the same conditions as for
dependent functions, but the introduction rule Lam-Ir checks the body assuming
the parameter is irrelevant.

We can eliminate a term of intersection type by applying it to an expression
which is well-typed in the upgraded context ${\Gamma}^{\uparrow}$, i.e., which
may contain ghost variables, via the rule App-Ir. Similarly to the case for
dependent functions, reduction must be encoded as an axiom
$\beta_{\mathsf{ir}}$, where the ”$\mathsf{ir}$” stands for ”irrelevant.” We
may also introduce an _irrelevance axiom_ , Ir-Ty, which essentially says that
ghost arguments do not matter for the purposes of determining equality
whenever the ghost variable does not occur in the result type.

We move on to introduce dependent pair types with the type formation rule
Pair-WF. The introduction rule Pair looks a bit like the introduction rule for
sigma-types in dependent type theories, with the type of the second component
varying according to the first component, and both components computationally
relevant.

The elimination form is a let-binding form (in Let-Pair). We may also
eliminate into proofs using Let-Pair-Pr; note that, in this case, the
expression $e:(a:A)\times B$ may contain ghost variables (as it only needs to
be well-typed in ${\Gamma}^{\uparrow}$). As before, reduction for dependent
pair elimination must be encoded as an axiom, $\beta_{\mathsf{pair}}$.

Often, however, we may want to be able to consider, dually to intersection
types, _union types_ $\exists x:A,B(x)$ (Union-WF), which we may views as
dependent pairs conditioned on a ghost variable, or, set-theoretically, as
elements of $B(a)$ for some valid $a$. Similarly to for dependent pairs, we
support an introduction rule Pair-Ir, and elimination via let-binding using
rules Let-Ir and Let-Ir-Pr. Note that, unlike for dependent pairs, and
similarly to intersection types, $a$ only needs to be well-typed in
${\Gamma}^{\uparrow}$ (rather than $\Gamma$) in the introduction rule Pair-Ir,
while in Let-Ir, the binder $\|x:A\|$ is a ghost binder rather than a term
binder. Finally, as before, we also introduce a reduction rule for let-
bindings, $\beta_{\mathsf{ir}}$.

Just as dependent functions and pairs have corresponding type formers
quantifying over ghost variables rather than term variables, we may also
construct type formers predicated over propositions. In particular, we may
consider the _precondition type_ : essentially a closure yielding an element
of the type $A$ if the proposition $p$ is true; this has introduction rule
Pre-WF. Introduction is by abstracting a term over a proof variable, with rule
Lam-Pr. Note that the type $A$ in Lam-Pr is allowed to depend on a proof
$u:\varphi$; this is because we may consider precondition types
$({u}:{\varphi})\Rightarrow{A}$ in which $A$ is only well-formed if $\varphi$
holds. For example, consider a function $f:\\{X\mid\varphi(x)\\}\to X$ (we
will cover subset types shortly); to reason about values of $f$ for $a:X$, we
need $\varphi(a)$ to hold, hence, we require dependency on proofs to be able
to type $({u}:{\varphi(a)})\Rightarrow{\\{z:\\{y:X\mid\varphi(y)\\}\mid
f\;z=f\;\\{a,u\\}\\}}$. Similarly to for the computational and ghost variable
cases, we must also introduce a reduction rule $\beta_{\mathsf{pr}}$. Dually,
we may introduce the _subset type_ former Set-WF, representing, in essence,
elements $a$ of type $A$ satisfying the predicate $\varphi(a)$. This has the
expected introduction rule Set and supports elimination via let-binding with
rules Let-Set and Let-Set-Pr. We also introduce a reduction rule,
$\beta_{\mathsf{set}}$, as expected.

Currently, we have the ability to manipulate data and associate it with
propositions, but do not yet have any bona fide data types. While there is no
semantic obstacle to introducing a full language of datatype declarations, for
simplicity, we will restrict ourselves to the unit type, sum types, and the
natural numbers. Other inductive types follow a similar pattern. As usual, a
value of the unit type may be introduced with rule Unit; rather than the
eliminator we would expect from dependent type theory, we may simply couple
this with an axiom, Uniq, stating that every member of the unit type is equal
to $()$. While on it’s own this is not a particularly interesting datatype,
when combined with coproduct types $A+B$, we may define, for example, the type
of Booleans as $\mathbf{2}\equiv\mathbf{1}+\mathbf{1}$, allowing us to
construct finite types. Coproducts may be introduced via injection (via rules
Inl and Inr) and eliminated by case splitting (via rules Cases and Cases-Pr).
To demonstrate support for infinite types, we introduce the natural numbers
$\mathbb{N}$, constants of which may be built up using Zero and Succ. The
elimination rule, Natrec, implements essentially iteration with the current
step available as a _ghost_ variable (for reasoning about in propositions);
it’s computational semantics are given by the axioms $\beta_{\mathsf{zero}}$
and $\beta_{\mathsf{succ}}$. Furthermore, just as we may construct terms
recursively via $\mathsf{natrec}$, we may also perform proofs by induction via
$\mathsf{ind}$ using rule Ind. Note that, unlike in Natrec, the expression $n$
over which we are performing induction is allowed to contain ghost variables.

####  4.2.3. Propositional Structure

Now that we have given essentially a complete description of the
$\lambda_{\mathsf{ert}}$’s terms and their computational behaviour, we can
describe the main components of $\lambda_{\mathsf{ert}}$’s propositional
logic, which for the most part mirror the term formers, since we encode proofs
in first-order logic as $\lambda$-terms via the Curry-Howard correspondence.
We begin by introducing propositions $\top$ and $\bot$; the former is only
equipped with introduction rule True, whereas $\bot$, being an initial object,
is only equipped with the elimination rules Absurd-Pr and Absurd. The latter
rule is especially important, as it is the main way with which our logic is
capable of interacting with our term calculus by allowing us to safely erase
unreachable branches from, e.g., a $\mathsf{natrec}$ or $\mathsf{cases}$
expression.

Proofs of equality do not interact meaningfully with the term calculus, since
they are logical formulae, and our logic is classical and nonconstructive. So
principles such as unique choice (which permit turning a proof that there
exists a unique element of type $A$ into a computational value of type $A$)
are not valid. The only case in which this is allowable is for the empty type
(see the discussion of the Absurd rule above). To make use of this, we need
the additional axiom Discr, which essentially says that the right-hand and
left-hand side of a coproduct type are disjoint. This suffices to effectively
introduce disequality into our type theory, as desired.

We may now introduce the rest of the connectives of first-order logic,
suitably modified in order to fit our setting. In particular, we have
_implication_ $({u}:{\varphi})\Rightarrow{\psi}$, which, as per the Curry-
Howard correspondence, is introduced by abstracting over a proposition
variable, via rule Imp, and eliminated via modus ponens (under Curry-Howard,
application) MP. Similarly, we have _conjunction_ $(u:\varphi)\land\psi$,
which is introduced by constructing a pair, via rule And, and eliminated via a
let-binding, with rule Let-And. We note that both associated proposition
formers, Imp-WF and And-WF, are ”dependent,” in that their right-hand side
$\psi$ is allowed to depend on a proof variable $u$ for the left-hand side
$\varphi$. This is because we allow the case where $\psi$ is not well-formed
without $\varphi$ holding (for example, because it is about a term that
requires a proof of $\varphi$). On the other hand, similarly to for
coproducts, the rules for disjunction $\varphi\lor\psi$ are simpler, with
introduction by injection via rules Orl and Orr, and elimination via case
splitting with rule Cases-Or.

Finally, just as we may consider a type quantifying over a proposition, to
support full first-order logic, we must also be able to consider propositions
quantified over types. In particular, we may introduce _universally
quantified_ propositions with formation rule Univ-Wf. These may be introduced
by generalization via rule Gen, and specialized via elimination rule Spec.
Similarly, we may introduce _existentially quantified_ propositions with
formation rule Exists-WF. We introduce proofs of an existentially quantified
proposition by introducing a witness via rule Wit, and may eliminate proofs
via let-binding with rule Let-Exists. Note in particular that, in both cases,
we treat the variable being quantified over as a _ghost_ variable, since it is
appearing in a proposition. Furthermore, since propositions have no
computational semantics, a reduction rule is unnecessary for either.

Altogether, our $\beta$ and $\eta$ rules are quite powerful, enabling us to
prove more extensionality properties than a casual look at the axioms may
suggest. In particular, fixing a term $e$ with free variable
$z:\\{x:A\mid\varphi\\}$, the $\eta$-rule for subsets can be written as:

(19)
$\begin{array}[]{rl}\eta_{\mathsf{set}}[C]&\equiv\hat{\lambda}\|a:\\{x:A\mid\varphi\\}\|,\mathsf{let}\;\\{y,v\\}=a\;\mathsf{in}\;\beta_{\mathsf{set}}\;\\{y,v\\}\;((x,u)\mapsto([\\{x,u\\}/z]e))\\\
&:\forall
a:\\{x:A\mid\varphi\\},\mathsf{let}\;\\{x,u\\}=a\;\mathsf{in}\;[\\{x,u\\}/z]e=[a/z]e\end{array}$

(note that $a,x,u,y,v$ are assumed to be fresh variables here). In general, we
only need to introduce explicit extensionality axioms for intersection types
($\eta_{\mathsf{ir}}$) and precondition types ($\eta_{\mathsf{pr}}$), with all
the other $\eta$ and extensionality rules we would expect to hold being
derivable from the rest of the axioms, with the sole exception of function
extensionality, which is not compatible with our current semantics. See
section 5.3 for the explanation of why.

Overall, $\lambda_{\mathsf{ert}}$’s logic is essentially multi-sorted first-
order logic, with the sorts drawn from the types of $\lambda_{\mathsf{ert}}$’s
programming language. Since $\lambda_{\mathsf{ert}}$ has function types, this
means that the $\lambda_{\mathsf{ert}}$ logic is fairly close to
$\mathrm{PA}^{\omega}$, Peano arithmetic over the full type hierarchy. So any
property provable about $\lambda_{\mathsf{ert}}$ terms with first-order logic
and induction should be provable. (We have not proved any theorems about the
expressivity of $\lambda_{\mathsf{ert}}$’s logic, though.)

###  4.3. Syntactic Metatheory

$\lambda_{\mathsf{ert}}$ satisfies the expected syntactic properties of
substitution and regularity. To show this, we define substitutions as
functions $\sigma:\mathsf{Var}\to\mathsf{Term}\uplus\mathsf{Proof}$, and can
recursively define capture-avoiding substitution on terms/proofs $e$, written
$[\sigma]e$, in the obvious way. We define a well-formed substitution from
$\Gamma$ to $\Delta$, written $\Gamma\vdash^{\prime}\sigma:\Delta$, as a
substitution satisfying the following conditions:

(20) $\displaystyle\implies\Delta\vdash\sigma\;x:[\sigma]A$
$\displaystyle[(u:\varphi)\in\Gamma]$
$\displaystyle\implies\Delta\vdash\sigma\;u:[\sigma]\varphi$
$\displaystyle[\|x:A\|\in\Gamma]$
$\displaystyle\implies[\|\sigma\;x:[\sigma]A\|\in\Delta]\lor[\Delta\vdash\sigma\;x:[\sigma]A]$

Furthermore, we say $\sigma$ is a _strict_ substitution, written
$\Gamma\vdash\sigma:\Delta$, if ghost variables in $\Gamma$ are only replaced
with ghost variables in $\Delta$.

###### Lemma 4.3 (Syntactic Substitution).

If $\Gamma\vdash^{\prime}\sigma:\Delta$ and $\Gamma\vdash a:A$, then
$\Delta\vdash[\sigma]a:[\sigma]A$.

_Formalized as: LogicalRefinement/Typed/Subst.lean, theorem HasType.subst’_

The proof of substitution is a routine induction, which as usual requires
first proving weakening. Once we know that substitution holds, we can prove
regularity:

###### Lemma 4.4 (Syntactic Regularity).

If $\Gamma\vdash a:A$, then $\Gamma\vdash A\;\mathsf{ty}$. Also, if
$\Gamma\vdash p:\varphi$, then $\Gamma\vdash\varphi\;\mathsf{pr}$.

_Formalized as: LogicalRefinement/Typed/Regular.lean, theorem HasType.regular_

This requires syntactic substitution since some of the typing rules (such as
App) involve a substitution in the result types. One other result we will use
later is that substitutions can be upgraded; that is,
$\Gamma\vdash\sigma:\Delta\implies{\Gamma}^{\uparrow}\vdash\sigma:{\Delta}^{\uparrow}$.
To avoid confusion, we write the latter as
${\Gamma}^{\uparrow}\vdash{\sigma}^{\uparrow}:{\Delta}^{\uparrow}$, with the
upgrade on substitutions taken to be the identity.

##  5\. Semantics

To give a denotational semantics for the $\lambda_{\mathsf{ert}}$ calculus, we
first show that all the proofs and dependencies in an $\lambda_{\mathsf{ert}}$
term can be erased in a compositional way. This yields a simple type for each
$\lambda_{\mathsf{ert}}$ type, and a simply-typed term for each
$\lambda_{\mathsf{ert}}$ term. We then give a semantics for each
$\lambda_{\mathsf{ert}}$ type as a subset of the denotational semantics of the
erasure for that type. Finally, we show that each well-typed
$\lambda_{\mathsf{ert}}$ term lies in the subset defined by its type.

In section 5.1, we recall the syntax and semantics of the simply-typed lambda
calculus. In section 5.2, we give an erasure function from
$\lambda_{\mathsf{ert}}$ types and terms to $\lambda_{\mathsf{stlc}}$ types
and terms respectively, and prove some expected properties like preservation
of well-typedness and semantic substitution (where the denotational semantics
of an $\lambda_{\mathsf{ert}}$ term are taken to be the semantics of its
erasure). Finally, in section 5.3, we give a semantics to
$\lambda_{\mathsf{ert}}$ types by assigning each a subset, and show that the
denotations of all well-typed $\lambda_{\mathsf{ert}}$ terms lie in the subset
assigned to their type, i.e., semantic regularity. From this, we deduce that
”well typed programs don’t go wrong”.

For the more categorically-minded reader, we interpret
$\lambda_{\mathsf{stlc}}$ in the Kleisli category of the exception monad
$M(X)$ (in the category of sets), and then interpret $\lambda_{\mathsf{ert}}$
in terms of the subset fibration over it. That is, an $\lambda_{\mathsf{ert}}$
type can be understood as a pair $(X,P\subseteq X)$, where $X$ is a type of
$\lambda_{\mathsf{stlc}}$, and $P$ is a predicate on that type; and
$\lambda_{\mathsf{ert}}$ terms are maps
$f\in(\Gamma,P_{\Gamma})\to(M(X),P_{M(X)})$ such that for all $\gamma\in
P_{\Gamma}$, we have $f(\gamma)\in P_{M(X)}$. Semantically, our erasure
operation amounts to the forgetful functor into the Kleisli category which
drops the property information.

###  5.1. The Simply-Typed Lambda Calculus

We begin by providing typing rules for $\lambda_{\mathsf{stlc}}$ in figure 10
(a formal grammar is provided in figure 16 in the appendix). This is a
standard lambda calculus with functions, sums, products, natural numbers, as
well as a simple effect: error stops. We define $\mathsf{Term}_{\lambda}$ to
be the set of $\lambda_{\mathsf{stlc}}$ terms. Similarly to the
$\lambda_{\mathsf{ert}}$ calculus, given a function
$\sigma:\mathsf{Var}\to\mathsf{Term}_{\lambda}$, we may then recursively
define (capture-avoiding) substitution of a term $t$ in the usual manner. We
say that $\sigma$ is a substitution from $\Gamma$ to $\Delta$, written
$\Gamma\vdash_{\lambda}\sigma:\Delta$, if it satisfies the property that
$(a:A)\in\Gamma\implies\Delta\vdash_{\lambda}\sigma\;a:A$.

We may then state the usual property of syntactic substitution as follows:

###### Lemma 5.1 (Syntactic Substitution ($\lambda_{\mathsf{stlc}}$)).

Given a substitution $\Gamma\vdash_{\lambda}\sigma:\Delta$ and
$\Gamma\vdash_{\lambda}t:A$, we have $\Delta\vdash_{\lambda}[\sigma]t:A$

_Formalized as: LogicalRefinement/Stlc/Basic.lean, theorem Stlc.HasType.subst_

We may now give $\lambda_{\mathsf{stlc}}$ a denotational semantics. Fixing the
exception monad $\mathsf{M}$, with exception $\mathsf{error}$, we begin by
giving denotations for $\lambda_{\mathsf{stlc}}$ types in figure 11, using
Moggi’s call-by-value semantics for types (Moggi, 1991). We may then define
the denotation of an $\lambda_{\mathsf{stlc}}$ context elementwise by taking
$\llbracket{\cdot}\rrbracket=\mathbf{1}$,
$\llbracket{\Gamma,x:A}\rrbracket=\llbracket{\Gamma}\rrbracket\times\mathsf{M}\;\llbracket{A}\rrbracket$.
Despite the fact that our semantics is call-by-value, the interpretation of
each hypothesis lives in the monad $\mathsf{M}$. We do this so our
denotational semantics can interpret substituting arbitrary terms for
variables, and not just values for variables. (Since the substitution rule
permits substituting arbitrary terms for variables, our semantics has to
support this too.) For each variable $x:A$ in a context $\Gamma$, we define
pointwise projections
$\pi_{x}:\llbracket{\Gamma}\rrbracket\to\llbracket{A}\rrbracket$. We define
(in figure 12) the denotation of a derivation $\Gamma\vdash_{\lambda}a:A$ as a
function of type
$\llbracket{\Gamma}\rrbracket\to\mathsf{M}(\llbracket{A}\rrbracket)$, which
takes environments (elements of $\llbracket{\Gamma}\rrbracket$) to elements of
the monadic type $\mathsf{M}(\llbracket{A}\rrbracket)$.

We can now give a relatively straightforward account of the denotational
semantics of an $\lambda_{\mathsf{stlc}}$ substitution as follows: we
interpret a substitution $\Gamma\vdash_{\lambda}\sigma:\Delta$ as a function
$\llbracket{\Gamma\vdash_{\lambda}\sigma:\Delta}\rrbracket:\llbracket{\Delta}\rrbracket\to\llbracket{\Gamma}\rrbracket$
by composing it elementwise with the the denotational semantics. Supposing
$D\in\llbracket{\Delta}\rrbracket$:

(21)
$\pi_{x,\Gamma}(\llbracket{\Gamma\vdash_{\lambda}\sigma:\Delta}\rrbracket\;D)=\llbracket{\Delta\vdash_{\lambda}\sigma\;x:A}\rrbracket\;D\in\llbracket{A}\rrbracket$

We may now state semantic substitution for the $\lambda_{\mathsf{stlc}}$ as
follows:

###### Lemma 5.2 (Semantic Substitution ($\lambda_{\mathsf{stlc}}$)).

Given $\lambda_{\mathsf{stlc}}$ derivation $\Gamma\vdash_{\lambda}a:A$ and
$\lambda_{\mathsf{stlc}}$ substitution $\Gamma\vdash_{\lambda}\sigma:\Delta$,
we have

$\llbracket{\Gamma\vdash_{\lambda}a:A}\rrbracket\circ\llbracket{\Gamma\vdash_{\lambda}\sigma:\Delta}\rrbracket=\llbracket{\Delta\vdash_{\lambda}[\sigma]a:[\sigma]A}\rrbracket$

_Formalized as: LogicalRefinement/Stlc/Subst.lean, theorem
Stlc.HasType.subst_interp_dist_

$\displaystyle\prftree{}{\Gamma\vdash_{\lambda}():\mathbf{1}}\qquad\prftree{}{\Gamma\vdash_{\lambda}\mathsf{error}:A}\qquad\prftree{\Gamma\vdash_{\lambda}a:A}{\Gamma,x:A\vdash_{\lambda}e:B}{\Gamma\vdash_{\lambda}\mathsf{let}\;x=a\;\mathsf{in}\;e:B}$
$\displaystyle\prftree{\Gamma,x:A\vdash_{\lambda}e:B}{\Gamma\vdash_{\lambda}\lambda
x:A,e:A\to B}\qquad\prftree{\Gamma\vdash_{\lambda}f:A\to
B}{\Gamma\vdash_{\lambda}a:A}{\Gamma\vdash_{\lambda}f\
a:B}\qquad\prftree{\Gamma\vdash_{\lambda}l:A}{\Gamma\vdash_{\lambda}r:B}{\Gamma\vdash_{\lambda}(l,r):A\times
B}$
$\displaystyle\prftree{\Gamma\vdash_{\lambda}e:A}{\Gamma\vdash_{\lambda}\mathsf{inl}\;e:A+B}\qquad\prftree{\Gamma\vdash_{\lambda}e:B}{\Gamma\vdash_{\lambda}\mathsf{inr}\;e:A+B}\qquad\prftree{\Gamma\vdash_{\lambda}e:A+B}{\Gamma,x:A\vdash_{\lambda}l:C}{\Gamma,y:B\vdash_{\lambda}r:C}{\Gamma\vdash_{\lambda}\mathsf{cases}\;e\;(\mathsf{inl}\;x\mapsto
l)\;(\mathsf{inr}\;y\mapsto r):C}$
$\displaystyle\prftree{}{\Gamma\vdash_{\lambda}0:\mathbb{N}}\qquad\prftree{}{\Gamma\vdash_{\lambda}\mathsf{succ}:\mathbb{N}\to\mathbb{N}}\qquad\prftree{\Gamma\vdash_{\lambda}e:\mathbb{N}}{\Gamma\vdash_{\lambda}z:C}{\Gamma,x:C\vdash_{\lambda}s:C}{\Gamma\vdash_{\lambda}\mathsf{natrec}\;e\;z\;(x\mapsto
s):C}$

Figure 10. $\lambda_{\mathsf{stlc}}$ typing rules

STLC typing rules

$\displaystyle\llbracket{\mathbf{0}}\rrbracket=\\{\\},\qquad\llbracket{\mathbf{1}}\rrbracket=\\{*\\},\qquad\llbracket{\mathbb{N}}\rrbracket=\mathbb{N}$
$\displaystyle\llbracket{A\to
B}\rrbracket=\llbracket{A}\rrbracket\to\mathsf{M}\llbracket{B}\rrbracket,\qquad\llbracket{A+B}\rrbracket=\llbracket{A}\rrbracket\sqcup\llbracket{B}\rrbracket,\qquad\llbracket{A\times
B}\rrbracket=\llbracket{A}\rrbracket\times\llbracket{B}\rrbracket$

Figure 11. $\lambda_{\mathsf{stlc}}$ type denotations parameterized by a monad
$\mathsf{M}$. The denotation of a term of type $A$ has type
$\mathsf{M}\llbracket{A}\rrbracket$.

STLC type denotations parameterized by the exception monad M

$\boxed{\llbracket{\Gamma\vdash_{\lambda}a:A}\rrbracket:\llbracket{\Gamma}\rrbracket\to\mathsf{M}\;\llbracket{A}\rrbracket}$

$\displaystyle\llbracket{\Gamma\vdash_{\lambda}x:A}\rrbracket\;G={}$
$\displaystyle\pi_{x,\Gamma}G$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}():\mathbf{1}}\rrbracket\;G={}$
$\displaystyle\mathsf{ret}\;()$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}\mathsf{error}:A}\rrbracket\;G={}$
$\displaystyle\mathsf{error}_{A}$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}\lambda x:A,e:A\to
B}\rrbracket\;G={}$ $\displaystyle\mathsf{ret}\;(\lambda
a,\llbracket{\Gamma,x:A\vdash_{\lambda}e:B}\rrbracket(G,\mathsf{ret}\;a))$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}f\;a:B}\rrbracket\;G={}$
$\displaystyle\mathsf{bind}\;(\llbracket{\Gamma\vdash_{\lambda}f:(x:A)\to
B}\rrbracket\;G)\;(\lambda
f,\mathsf{bind}\;(\llbracket{\Gamma\vdash_{\lambda}a:A}\rrbracket\;G)\;f)$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}(l,r):A\times
B}\rrbracket\;G={}$
$\displaystyle\mathsf{bind}\;(\llbracket{\Gamma\vdash_{\lambda}l:A}\rrbracket\;G)\;(\lambda
l,\mathsf{bind}\;(\llbracket{\Gamma\vdash_{\lambda}r:B}\rrbracket\;G)\;(\lambda
r,\mathsf{ret}\;(l,r)))$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}\mathsf{inl}\;e:A+B}\rrbracket\;G={}$
$\displaystyle\mathsf{fmap}\;\mathsf{inl}\;(\llbracket{\Gamma\vdash_{\lambda}e:A}\rrbracket\;G)$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}\mathsf{inr}\;e:A+B}\rrbracket\;G={}$
$\displaystyle\mathsf{fmap}\;\mathsf{inr}\;(\llbracket{\Gamma\vdash_{\lambda}e:B}\rrbracket\;G)$
$\displaystyle\left\llbracket{\begin{array}[]{ll}\Gamma\vdash_{\lambda}&\mathsf{cases}\;d\\\
&\quad(\mathsf{inl}\;y\mapsto l)\\\ &\quad(\mathsf{inr}\;z\mapsto
r):C\end{array}}\right\rrbracket\;G={}$
$\displaystyle\left({\begin{array}[]{l}\mathsf{bind}\;(\llbracket{\Gamma\vdash_{\lambda}d:A+B}\rrbracket\;G)\;(\lambda
d,\\\ \quad\mathsf{cases}\;d\\\
\qquad(\mathsf{inl}\;a\mapsto\llbracket{\Gamma,y:A\vdash_{\lambda}l:C}\rrbracket\;(G,\mathsf{ret}\;a))\\\
\qquad(\mathsf{inr}\;b\mapsto\llbracket{\Gamma,z:B\vdash_{\lambda}r:C}\rrbracket\;(G,\mathsf{ret}\;b))\end{array}}\right)$
$\displaystyle\llbracket{0}\rrbracket\;G={}$ $\displaystyle\mathsf{ret}\;0$
$\displaystyle\llbracket{\mathsf{succ}}\rrbracket\;G={}$
$\displaystyle\mathsf{ret}\;\mathsf{succ}$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}\mathsf{natrec}\;n\;z\;(x\mapsto
s):C}\rrbracket\;G={}$
$\displaystyle\left({\begin{array}[]{l}\mathsf{bind}\;(\llbracket{\Gamma\vdash_{\lambda}n:\mathbb{N}}\rrbracket\;G)\;(\lambda
n,\\\
\quad\mathsf{natrec}\;n\;(\llbracket{\Gamma\vdash_{\lambda}z:C}\rrbracket\;G)\\\
\qquad(c\mapsto\mathsf{bind}\;c\;(\lambda c.\llbracket{\Gamma,x:C\vdash
s:C}\rrbracket(G,\mathsf{ret}\;c)))\end{array}}\right)$
$\displaystyle\llbracket{\Gamma\vdash_{\lambda}\mathsf{let}\;x=a\;\mathsf{in}\;e:B}\rrbracket\;G={}$
$\displaystyle\mathsf{bind}\;(\llbracket{\Gamma\vdash_{\lambda}a:A}\rrbracket\;G)\;(\lambda
a^{\prime},\llbracket{\Gamma,x:A\vdash_{\lambda}e:B}\rrbracket(G,\mathsf{ret}\;a^{\prime}))$

Figure 12.  Denotations for $\lambda_{\mathsf{stlc}}$ terms, where
$\mathsf{M}$ is the exception monad with $\mathsf{error}_{A}:\mathsf{M}\;A$

Denotations for STLC terms

###  5.2. Erasure

We define a notion of erasure $|A|$ of $\lambda_{\mathsf{ert}}$ types and
terms to corresponding $\lambda_{\mathsf{stlc}}$ ones in figure 13. Erasure on
types simply erases all dependency and propositional information leaving
behind a simply-typed skeleton. For tuple-like type formers like
$\left\\{{x}:{A}\mid{\varphi}\right\\}$, the propositional information is
erased completely, yielding $|A|$, whereas for function-like type formers like
$({u}:{\varphi})\Rightarrow{A}$, it is instead erased to a unit, yielding
$\mathbf{1}\to|A|$; this is to avoid issues with eager evaluation. Where
necessary, we take proofs and propositions to erase into the unit as a
convenience, i.e.,

(22)
$\forall\varphi\in\mathsf{Prop},|{\varphi}|=\mathbf{1}\in\mathsf{Type}_{\lambda},\qquad\forall
p\in\mathsf{Proof},|{p}|=()\in\mathsf{Term}_{\lambda}$

We may then recursively define the erasure of an $\lambda_{\mathsf{ert}}$
context into an $\lambda_{\mathsf{stlc}}$ context as follows:

(23)
$|{\cdot}|=\cdot,\qquad|{\Gamma,x:A}|=|{\Gamma}|,x:|{A}|\qquad|{\Gamma,u:\varphi}|=|{\Gamma}|,u:\mathbf{1}\qquad|{\Gamma,\|x:A\|}|=|{\Gamma}|,x:\mathbf{1}$

As one would expect; erasing a well-typed $\lambda_{\mathsf{ert}}$ term yields
a well-typed $\lambda_{\mathsf{stlc}}$ term; in particular, we have that:

###### Lemma 5.3 (Erasure).

Given a derivation $\Gamma\vdash a:A$, we may derive a derivation of
$|{\Gamma}|\vdash_{\lambda}|{a}|:|{A}|$, written $|{\Gamma\vdash a:A}|$

_Formalized as: LogicalRefinement/Stlc/Interp.lean, theorem HasType.stlc_

With this definition in hand, we may define the erasure of a substitution
pointwise, that is, as

(24)
$\forall\sigma\in\mathsf{Var}\to\mathsf{Term},|{\sigma}|\;a=|{\sigma\;a}|$

It then follows as a trivial corollary of lemma 5.3 that, given a substitution
$\Gamma\vdash\sigma:\Delta$, we have
$|{\Gamma}|\vdash_{\lambda}|{\sigma}|:|{\Delta}|$; we write this as
$|{\Gamma\vdash\sigma:\Delta}|$. We are now in a position to prove that the
erasure of the substitution of an $\lambda_{\mathsf{ert}}$ term is the erased
substitution of the corresponding erased $\lambda_{\mathsf{stlc}}$ term:

###### Lemma 5.4 (Substitution and Erasure Commute).

Given a substitution $\Gamma\vdash\sigma:\Delta$, we have
$|{[\sigma]a}|=[|{\sigma}|]|{a}|$

_Formalized as: LogicalRefinement/Stlc/InterpSubst.lean, theorem
HasType.subst_stlc_commute_

We may then deduce the following corollary from lemma 5.2 and lemma 5.4:

###### Corollary 5.5 (Substitution and Erasure Denotation Commute).

Given $\lambda_{\mathsf{ert}}$ derivation $\Gamma\vdash a:A$ and
$\lambda_{\mathsf{ert}}$ substitution $\Gamma\vdash\sigma:\Delta$, we have

$\llbracket{|{\Gamma\vdash
a:A}|}\rrbracket\circ\llbracket{|{\Gamma\vdash\sigma:\Delta}|}\rrbracket=\llbracket{|{\Delta\vdash[\sigma]a:[\sigma]A}|}\rrbracket$

_Formalized as: LogicalRefinement/Stlc/InterpSubst.lean, theorem
HasType.subst_stlc_commute_

$\boxed{|{\cdot}|:\mathsf{Type}\to\mathsf{Type}_{\lambda}}$

$\displaystyle|{(x:A)\to B}|=|{A}|\to|{B}|,\qquad|{(x:A)\times
B}|=|{A}|\times|{B}|$
$\displaystyle|{({u}:{\varphi})\Rightarrow{A}}|=\mathbf{1}\to|{A}|,\qquad|{\left\\{{x}:{A}\mid{\varphi}\right\\}}|=|{A}|,\qquad|{\forall
x:A,B}|=\mathbf{1}\to|{B}|,\qquad|{\exists x:A,B}|=|{B}|$
$\displaystyle|{\mathbf{1}}|=\mathbf{1},\qquad|{A+B}|=|{A}|+|{B}|,\qquad|{\mathbb{N}}|=\mathbb{N}$

$\boxed{|{\cdot}|:\mathsf{Term}\to\mathsf{Term}_{\lambda}}$

$\displaystyle|{x}|=x\qquad|{\lambda x:A,e}|=\lambda
x:|{A}|.|{e}|\qquad|{a\;b}|=|{a}|\;|{b}|,\qquad|{(a,b)}|=(|{a}|,|{b}|)$
$\displaystyle|{\mathsf{let}\;(x,y):A=e\;\mathsf{in}\;e^{\prime}}|=\mathsf{let}\;(x,y)=|{e}|\;\mathsf{in}\;|{e^{\prime}}|,\qquad|{\mathsf{inl}\;e}|=\mathsf{inl}\;|{e}|,\qquad|{\mathsf{inr}\;e}|=\mathsf{inr}\;|{e}|$
$\displaystyle|{\mathsf{cases}[x\mapsto C]\;e\;(\mathsf{inl}\;y\mapsto
l)\;(\mathsf{inr}\;z\mapsto
r)}|=|{\mathsf{cases}\;e\;(\mathsf{inl}\;y\mapsto|{l}|)\;(\mathsf{inr}\;z\mapsto|{r}|)}|$
$\displaystyle|{\lambda
u:\varphi,e}|=\lambda\\_:\mathbf{1}.|{e}|,\qquad|{a\;p}|=|{a}|\;(),\qquad|{\\{a,p\\}}|=|{a}|$
$\displaystyle|{\mathsf{let}\;\\{x,y\\}:A=e\;\mathsf{in}\;e^{\prime}}|=\mathsf{let}\;x=|{e}|\;\mathsf{in}\;|{e^{\prime}}|$
$\displaystyle|{\lambda\|x:A\|,e}|=\lambda\\_:\mathbf{1}.|{e}|,\qquad|{a\;\|b\|}|=|{a}|\;(),\qquad|{(\|a\|,b)}|=|{b}|$
$\displaystyle|{\mathsf{let}\;(\|x\|,y):A=e\;\mathsf{in}\;e^{\prime}}|=\mathsf{let}\;y=|{e}|\;\mathsf{in}\;|{e^{\prime}}|$
$\displaystyle|{0}|=0\qquad|{\mathsf{succ}}|=\mathsf{succ}\qquad|{\mathsf{natrec}[x\mapsto
C]\;e\;z\;(\|\mathsf{succ}\;n\|,y\mapsto
b)}|=\mathsf{natrec}\;|{e}|\;|{z}|\;(y\mapsto|{b}|)$
$\displaystyle|{\mathsf{absurd}\;p}|=\mathsf{error}$

Figure 13. Erasure of $\lambda_{\mathsf{ert}}$ to $\lambda_{\mathsf{stlc}}$

Erasure of ERT to STLC

###  5.3. Denotational Semantics

Using lemma 5.3, we could assign a computational meaning to well-typed
$\lambda_{\mathsf{ert}}$ terms $\Gamma\vdash t:A$ by simply composing the
denotation for $\lambda_{\mathsf{stlc}}$ terms with the erasure function,
i.e., taking $\llbracket{|{\Gamma\vdash
t:A}|}\rrbracket:\llbracket{|{\Gamma}|}\rrbracket\to\mathsf{M}\llbracket{|{A}|}\rrbracket$.
While this interpretation assigns terms a computational meaning, it simply
ignores their refinements: there is not yet any guarantee that the refinements
mean anything.

To rectify this, we will give a denotational semantics for
$\lambda_{\mathsf{ert}}$ types (in figure 14), which maps each type to a
subset of the denotation of the corresponding erased type. This semantics is
mutually recursive with semantics for $\lambda_{\mathsf{ert}}$ propositions as
well.

The denotation of types (and propositions) is parameterized by an environment
$G$ drawn from the interpretation of the context $\Gamma$. To break the
recursion between the semantics of contexts and types, the domain of the
interpretation function for types (and propositions) is not restricted to
valid $\lambda_{\mathsf{ert}}$ environments
$G\in\llbracket{\Gamma\;\mathsf{ok}}\rrbracket$, but is defined for all
$\lambda_{\mathsf{stlc}}$ environments $G\in\llbracket{|{\Gamma}|}\rrbracket$.
However, the semantics of $\lambda_{\mathsf{ert}}$ types does depend upon the
values of ghost variables. As a result, we do not consider the erasure
$|{\Gamma}|$, but rather the erasure of the _upgrade_
$|{{\Gamma}^{\uparrow}}|$.

The denotation of types basically follows the structure of a unary logical
relation (i.e., a logical predicate). For example, the intepretation
$\llbracket{\Gamma\vdash(x:A)\to B}\rrbracket\;G$ are functions
$|{A}|\to\mathsf{M}(|{B}|)$ which satisfy the property that for all inputs in
the refined type $A$, the function returns a pure value in the refined type
$B$. An element of a pair $(x:A)\times B[x]$ is a pair $(a,b)$ in
$|{A}|\times|{B}|$ where $a$ is an element of $A$ and $b$ is an element of
$B[a]$.

The union type $\exists x:A,B[x]$ are those elements of $|B|$ which lie in
$B[a]$ for some $a$ in $A$. The intersection type $\forall x:A,B$ is almost
dual, but to account for call-by-value evaluation in the case where $A$ may be
an empty type, we consider thunks $1\to\mathsf{M}(|{B}|)$ rather than elements
of $|{B}|$. This is also where the terms ”intersection type” and ”union type”
come from – the semantics of $\forall x:A,B$ is literally a giant
intersection, and likewise $\exists x:A,B[x]$ is interpreted with a giant
union.

An element of a subset type $\\{x:A\mid\varphi\\}$ is an element of $A$ which
also satisfies the property $\varphi$. The dual precondition type
$({u}:{\varphi})\Rightarrow{A}$ represents elements of $A$, conditional on
$\phi$ holding. Just as with intersections, this type must be represented by
thunks $1\to\mathsf{M}(|{A}|)$ to account for the case where $\varphi$ is
false. Units and natural numbers have the same denotation as their simply-
typed counterpart, and a coproduct $A+B$ is either a left injection of a value
satisfying $A$ or a right injection of a value satisfying $B$. A proposition
$\varphi$ could be interpreted by a map
$\llbracket{|{\Gamma}|}\rrbracket\to\mathbf{2}$, but it is more convenient to
think of it as a subset of $\llbracket{|{\Gamma}|}\rrbracket$ – the set of
contexts for which the proposition holds. So $\top$ is the whole set of
contexts, $\bot$ is the empty set, and disjunction and conjunction are
modelled by union and intersection. Because conjunction is written
$u:\varphi\land\psi[u]$, we have to extend the environment of the
interpretation of $\psi$. Since we erase all propositions to $\mathbf{1}$, we
just choose $\mathsf{ret}\;()$ as the erased proof. The same idea is used in
the case of propositional implication. Quantifiers in our language of
propositions are interpreted by quantifiers in the meta-language, and equality
is interpreted as the set of contexts
$G\in\llbracket{|{{\Gamma}^{\uparrow}}|}\rrbracket$ for which the equality
holds. Note in particular that this means that the law of the excluded middle
is sound, and cannot interfere with program execution in any way (since all
propositions are erased).

Because the unrefined language is ambiently effectful (with the effect of
error stops), every expression lies in a monadic type in the semantics. The
refined semantics of the monad is given by the
$\mathcal{E}\llbracket{\Gamma\vdash A\;\mathsf{ty}}\rrbracket$ relation, which
picks out the subset of the monad not equal to $\mathsf{error}_{A}$. That is,
we require all refined terms to terminate without error.

Propositions are interpreted as a map from the intepretation of contexts into
the (boolean, classical) truth values, or equivalently, as a subset of the
contexts. Hence each logical connective is interpreted by the corresponding
operation in the Boolean algebra of sets – conjunction is intersection,
disjunction is union, and so on. We interpret equality at a type $A$ as
equality of the underlying elements of $|A|$.

This interpretation, while simple, is in some sense _too_ simple – it causes
function extensionality to fail. In particular, suppose
$\mathsf{Pos}\equiv\\{x:\mathbb{Z}\mid x>0\\}$ is the type of positive
numbers. Two functions $f,g:\mathsf{Pos}\to\mathbb{Z}$ may agree on all
positive arguments but fail to be equal because they erase to two functions
which do different things on negative arguments. (For example, consider
$f=\mathsf{id}$ and $g=\mathsf{abs}$.) This is also the reason that the
$\eta_{\mathsf{ir}}$ and $\eta_{\mathsf{pr}}$ rules have an inhabitation
premise (e.g., ${\Gamma}^{\uparrow}\vdash i:A$). A more complex semantics
based on partial equivalence relations could let us resolve this issue, but we
preferred to stick with the simplest possible semantics for expository
reasons.

The semantics of types and propositions is defined over a bigger set of
contexts than just the valid ones, but once we have this semantics, we can use
it to define the valid contexts. Again, the interpretation
$\llbracket{\Gamma\;\mathsf{ok}}\rrbracket$ is going to be the subset of
$\llbracket{|{{\Gamma}^{\uparrow}}|}\rrbracket$ which satisfy all the
propositions and in which all the values lie within their
$\lambda_{\mathsf{ert}}$ types. So the empty context is inhabited by the empty
environment; the context $\Gamma,u:\varphi$ is inhabited by
$(G,\mathsf{ret}\;())$ when $G$ is in
$\llbracket{\Gamma\;\mathsf{ok}}\rrbracket$ and $\varphi$ is satisfied; and
$\Gamma,x:A$ is inhabited by $(G,\mathsf{ret}\;x)$ when
$G\in\llbracket{\Gamma\;\mathsf{ok}}\rrbracket$ and $x$ is in the (subset)
interpretation of $A$. (The case of ghost variables is the same as ordinary
variables, since we care about the values of ghost variables when interpreting
propositions in refined types.) It is easy to show that no
$\lambda_{\mathsf{ert}}$ type can contain any errors.

###### Lemma 5.6 (Convergence).

Given an $\lambda_{\mathsf{ert}}$ derivation $\Gamma\vdash A\;\mathsf{ty}$, we
have $\forall G,\mathsf{error}\notin\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G$

_Formalized as: LogicalRefinement/Denot/Basic.lean, theorem
HasType.denote_ty_non_null_

However, we give semantics to $\lambda_{\mathsf{ert}}$ _terms_ by erasure, and
so we have to connect the erased semantics of $\lambda_{\mathsf{ert}}$ terms
to these semantic types. Furthermore, the semantics of
$\lambda_{\mathsf{ert}}$ types cares about ghost values, but the semantics of
erased terms ignore ghost values.

To relate these two, we also need to define the corresponding notion of a
downgrade of an environment. Given an environment
$G\in\llbracket{|{{\Gamma}^{\uparrow}}|}\rrbracket$, we recursively define its
downgrade ${G}^{\downarrow}_{\Gamma}\in\llbracket{|{\Gamma}|}\rrbracket$,
written ${G}^{\downarrow}$ when $\Gamma$ is clear from context, as

(25)
${*}^{\downarrow}_{\cdot}=*,\qquad{(x,G)}^{\downarrow}_{u:\varphi,\Gamma}=(x,{G}^{\downarrow}_{\Gamma}),\qquad{(y,G)}^{\downarrow}_{x:A,\Gamma}=(y,{G}^{\downarrow}_{\Gamma}),\qquad{(y,G)}^{\downarrow}_{\|x:A\|,\Gamma}=(*,{G}^{\downarrow}_{\Gamma})$

Semantically, this discards all of the ghost information from an environment.
We may now state the primary theorems proven about the semantics of
$\lambda_{\mathsf{ert}}$, namely, semantic substitution and semantic
regularity.

###### Theorem 5.7 (Semantic Substitution).

Given $\lambda_{\mathsf{ert}}$ derivation $\Gamma\vdash A\;\mathsf{ty}$,
$\lambda_{\mathsf{ert}}$ substitution $\Gamma\vdash\sigma:\Delta$, and valid
environment $D\in\llbracket{\Delta\;\mathsf{ok}}\rrbracket$, we have

$\llbracket{\Delta\vdash[\sigma]A\;\mathsf{ty}}\rrbracket\;D=\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket(\llbracket{|{{\Gamma}^{\uparrow}\vdash{\sigma}^{\uparrow}:{\Delta}^{\uparrow}}|}\rrbracket\;D)$

_Formalized as: LogicalRefinement/Denot/Subst.lean, theorem
SubstCtx.subst_denot_

We can also show that for any well-typed $\lambda_{\mathsf{ert}}$ term, its
erasure lies in the interpretation of the $\lambda_{\mathsf{ert}}$ type. This
shows that every well-typed term satisfies the properties of its fancy type.

###### Theorem 5.8 (Semantic Regularity).

Given an $\lambda_{\mathsf{ert}}$ derivation $\Gamma\vdash a:A$, we have

$\forall
G\in\llbracket{\Gamma\;\mathsf{ok}}\rrbracket,\llbracket{|{\Gamma\vdash
a:A}|}\rrbracket\;{G}^{\downarrow}\in\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G$

_Formalized as: LogicalRefinement/Denot/Regular.lean, theorem HasType.denote_

Furthermore, it is an immediate corollary of lemma 5.6 and theorem 5.8 that
the $\lambda_{\mathsf{ert}}$ logic is consistent, since
$\left\\{x:1\mid\phi\right\\}$ is inhabited if and only if $\phi$ is true. It
is also a corollary that for any well-typed term $\Gamma\vdash a:A$, we have
that $\forall
G\in\llbracket{\Gamma\;\mathsf{ok}}\rrbracket,\llbracket{|{\Gamma\vdash
a:A}|}\rrbracket\;G\neq\mathsf{error}$. That is, ”well-typed programs do not
go wrong”.

$\boxed{\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket:\llbracket{|{{\Gamma}^{\uparrow}}|}\rrbracket\to\mathcal{P}(\llbracket{|{A}|}\rrbracket)}$

$\displaystyle\llbracket{\Gamma\vdash\mathbf{1}\;\mathsf{ty}}\rrbracket\;G={}$
$\displaystyle\\{()\\}$ $\displaystyle\llbracket{\Gamma\vdash(x:A)\to
B\;\mathsf{ty}}\rrbracket\;G={}$
$\displaystyle\\{f\in\llbracket{|{A}|}\rrbracket\to\mathsf{M}\llbracket{|{B}|}\rrbracket\mid\forall
x\in\llbracket{\Gamma\vdash A\;\mathsf{ty}}\rrbracket\;G,$
$\displaystyle\qquad f\;x\in\mathcal{E}\llbracket{\Gamma,x:A\vdash
B\;\mathsf{ty}}\rrbracket\;(G,\mathsf{ret}\;x)\\}$
$\displaystyle\llbracket{\Gamma\vdash(x:A)\times
B\;\mathsf{ty}}\rrbracket\;G={}$ $\displaystyle\\{(l,r)\mid
l\in\llbracket{\Gamma\vdash A\;\mathsf{ty}}\rrbracket\;G\land
r\in\llbracket{\Gamma,x:A\vdash
B\;\mathsf{ty}}\rrbracket\;(G,\mathsf{ret}\;l)\\}$
$\displaystyle\llbracket{\Gamma\vdash A+B\;\mathsf{ty}}\rrbracket\;G={}$
$\displaystyle\mathsf{inl}(\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G)\cup\mathsf{inr}(\llbracket{\Gamma\vdash
B\;\mathsf{ty}}\rrbracket\;G)$
$\displaystyle\llbracket{\Gamma\vdash({u}:{\varphi})\Rightarrow{A}\;\mathsf{ty}}\rrbracket\;G={}$
$\displaystyle\\{f\in\mathbf{1}\to\mathsf{M}\llbracket{|{A}|}\rrbracket\mid$
$\displaystyle\qquad
G\in\llbracket{\Gamma\vdash\varphi\;\mathsf{pr}}\rrbracket\implies
f\;()\in\mathcal{E}\llbracket{\Gamma,u:\varphi\vdash
A\;\mathsf{ty}}\rrbracket\;(G,\mathsf{ret}\;())\\}$
$\displaystyle\llbracket{\Gamma\vdash\left\\{{x}:{A}\mid{\varphi}\right\\}\;\mathsf{ty}}\rrbracket\;G={}$
$\displaystyle\\{a\in\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G\mid(G,a)\in\llbracket{\Gamma,x:A\vdash\varphi\;\mathsf{pr}}\rrbracket\\}$
$\displaystyle\llbracket{\Gamma\vdash\forall
x:A,B\;\mathsf{ty}}\rrbracket\;G={}$
$\displaystyle\\{f\in\mathbf{1}\to\mathsf{M}\llbracket{|{B}|}\rrbracket\mid$
$\displaystyle\qquad\forall x\in\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G,f\;()\in\mathcal{E}\llbracket{\Gamma,x:A\vdash
B\;\mathsf{ty}}\rrbracket\;(G,\mathsf{ret}\;x)\\}$
$\displaystyle\llbracket{\Gamma\vdash\exists
x:A,B\;\mathsf{ty}}\rrbracket\;G={}$
$\displaystyle\bigcup_{x\in\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G}\llbracket{\Gamma,x:A\vdash
B\;\mathsf{ty}}\rrbracket(G,\mathsf{ret}\;x)$
$\displaystyle\llbracket{\Gamma\vdash\mathbb{N}\;\mathsf{ty}}\rrbracket\;G={}$
$\displaystyle\mathbb{N}$ $\displaystyle\mathcal{E}\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket={}$ $\displaystyle\lambda
G,\mathsf{ret}\;(\llbracket{\Gamma\vdash_{\lambda}A\;\mathsf{ty}}\rrbracket\;G):\llbracket{|{{\Gamma}^{\uparrow}}|}\rrbracket\to\mathcal{P}(\mathsf{M}\llbracket{|{A}|}\rrbracket)$

$\boxed{\llbracket{\Gamma\vdash\varphi\;\mathsf{pr}}\rrbracket:\mathcal{P}(\llbracket{|{{\Gamma}^{\uparrow}}|}\rrbracket)}$

$\displaystyle\llbracket{\Gamma\vdash\top\;\mathsf{pr}}\rrbracket={}$
$\displaystyle\llbracket{|{{\Gamma}^{\uparrow}}|}\rrbracket$
$\displaystyle\llbracket{\Gamma\vdash\bot\;\mathsf{pr}}\rrbracket={}$
$\displaystyle\varnothing$
$\displaystyle\llbracket{\Gamma\vdash({u}:{\varphi})\Rightarrow{\psi}\;\mathsf{pr}}\rrbracket={}$
$\displaystyle\\{G\mid
G\in\llbracket{\Gamma\vdash\varphi\;\mathsf{pr}}\rrbracket\implies(G,\mathsf{ret}\;())\in\llbracket{\Gamma,u:\varphi\vdash\psi\;\mathsf{pr}}\rrbracket\\}$
$\displaystyle\llbracket{\Gamma\vdash(u:\varphi)\land\psi\;\mathsf{pr}}\rrbracket={}$
$\displaystyle\\{G\mid
G\in\llbracket{\Gamma\vdash\varphi\;\mathsf{pr}}\rrbracket\land(G,\mathsf{ret}\;())\in\llbracket{\Gamma,u:\varphi\vdash\psi\;\mathsf{pr}}\rrbracket\\}$
$\displaystyle\llbracket{\Gamma\vdash\varphi\lor\psi\;\mathsf{pr}}\rrbracket={}$
$\displaystyle\llbracket{\Gamma\vdash\varphi\;\mathsf{pr}}\rrbracket\cup\llbracket{\Gamma\vdash\psi\;\mathsf{pr}}\rrbracket$
$\displaystyle\llbracket{\Gamma\vdash\forall
x:A,\varphi\;\mathsf{pr}}\rrbracket={}$ $\displaystyle\\{G\mid\forall
x\in\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G,(G,\mathsf{ret}\;x)\in\llbracket{\Gamma,x:A\vdash\varphi\;\mathsf{pr}}\rrbracket\\}$
$\displaystyle\llbracket{\Gamma\vdash\exists
x:A,\varphi\;\mathsf{pr}}\rrbracket={}$ $\displaystyle\\{G\mid\exists
x\in\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G,(G,\mathsf{ret}\;x)\in\llbracket{\Gamma,x:A\vdash\varphi\;\mathsf{pr}}\rrbracket\\}$
$\displaystyle\llbracket{\Gamma\vdash a=_{A}b\;\mathsf{pr}}\rrbracket={}$
$\displaystyle\\{G\mid\llbracket{|{{\Gamma}^{\uparrow}\vdash
a:A}|}\rrbracket\;G=\llbracket{|{{\Gamma}^{\uparrow}\vdash
b:A}|}\rrbracket\;G\\}$

$\boxed{\llbracket{\Gamma\;\mathsf{ok}}\rrbracket:\mathcal{P}(\llbracket{|{{\Gamma}^{\uparrow}}|}\rrbracket)}$

$\displaystyle\llbracket{\cdot\;\mathsf{ok}}\rrbracket={}$
$\displaystyle\\{\cdot\\}$
$\displaystyle\llbracket{\Gamma,x:A\;\mathsf{ok}}\rrbracket=\llbracket{\Gamma,\|x:A\|\;\mathsf{ok}}\rrbracket={}$
$\displaystyle\\{(G,\mathsf{ret}\;x)\mid
G\in\llbracket{\Gamma\;\mathsf{ok}}\rrbracket\land x\in\llbracket{\Gamma\vdash
A\;\mathsf{ty}}\rrbracket\;G\\}$
$\displaystyle\llbracket{\Gamma,u:\varphi\;\mathsf{ok}}\rrbracket={}$
$\displaystyle(\llbracket{\Gamma\;\mathsf{ok}}\rrbracket\cap\llbracket{\Gamma\vdash\varphi\;\mathsf{pr}}\rrbracket)\times\mathsf{M}\mathbf{1}$

Figure 14. Denotations for $\lambda_{\mathsf{ert}}$

Denotations for $\lambda_{\mathsf{ert}}$

##  6\. Formal Verification

We have proved all the results stated in the previous sections in Lean 4. The
proof development is about 15.8 kLoC in length and is partially automated,
though there is much potential for further automation. In particular, lemmas
4.1, 4.2, and 4.3 are heavily automated, with one template tactic that applies
to most of the cases, whereas theorems 5.7 and 5.8 and lemmas 5.2, 5.4, and
5.5 had to be proved manually. These properties typically had lots of equality
coercions, which had to be plumbed manually because they are difficult to
automate. It is possible that with more experience with Lean tactics they
might also be automated, but we were not able to do so.

The formalized syntax and semantics are mostly the same as that presented in
this writeup. There are two main differences. First, we have implemented
variables using de-Bruijn indices. Second, we folded types, propositions,
terms, and proofs into a single inductive type to avoid mutual recursion,
which Lean 4 currently has poor support for.

This project was the first time the authors used Lean 4 for serious
formalization work. While we ran into numerous issues due to Lean still being
in active early-stage development, we found it to be a highly effective
formalization tool. One issue we ran into was very high memory usage and, in
some cases, timeouts, when using Lean’s simp tactic on complex pattern
matches. The addition of the dsimp tactic, after a discussion on the Lean 4
Zulip, mostly alleviated this, and performance has improved in later versions
of Lean. We otherwise found the quality of automation to be very good: even
though the authors are novices at Lean, we were able to easily maintain and
extend the proofs without needing to edit theorems proved via tactics. For
example, we originally forgot to include the Unit-WF axiom, but we were able
to include it with only minor edits to the manual theorems in about 30
minutes. As the formalization made heavy use of dependent types, we also ran
into many issues attempting to establish equalities between dependently typed
terms. However, in this case, we found Lean relatively easy to use compared to
other dependently-typed proof assistants based on dependent types, with our
experiments at Coq-based formalization running into similar issues.

##  7\. Discussion

##### Function Extensionality, Recursion and Effects

Our current semantics is inconsistent with function extensionality because two
functions must be equal over their entire, unrefined domain to satisfy the
denotation of the equality type. To support extensionality (and related types
like quotient types), we should be able to intepret the calculus via a
semantics based on partial equivalence relations, as in (Harper, 1992).

We also want to reason about the partial correctness and divergent programs.
Hence, it makes sense to add support for general recursive definitions,
including nonterminating definitions, by moving to a domain-theoretic
semantics (rather than the set-theoretic semantics we currently use). We also
want to extend the base language with more effects (such as store and IO) and
extend $\lambda_{\mathsf{ert}}$ to support fine-grained reasoning about them
via an effect system such as in (Katsumata, 2014).

##### Categorical Semantics

The motivating model of refinement types underlying our work is that of
(Melliès and Zeilberger, 2015), which equates type refinement systems with
functors from a category of typing derivations to a category of terms. In
essence, one can view our work as taking the setup in (Melliès and Zeilberger,
2015) and inlining all the categorical definitions for the case of the simply-
typed lambda calculus.

We would like to update our formalisation to work in terms of the categorical
semantics; this would let us to account for all of the extensions above at
once, without having to reprove theorems (such as semantics substitution and
regularity) for each modification.

Recently, Kura (2021) has studied the denotational semantics of a system of
refinements over Ahman’s variant of dependent call-by-push-value (Ahman,
2018). Kura also uses a fibrational semantics similar to the Zeilberger-
Mellies semantics (as well as Katsumata’s semantics of effect systems
(Katsumata, 2014)) to equip a dependent type theory with a subtype relation
arising from the entailment relation of first-order logic. Unlike
$\lambda_{\mathsf{ert}}$, the use of subtyping means that there are no
explicit proofs, and hence type checking is undecidable.

##### Units in the Erasure

The erasure function for $\lambda_{\mathsf{ert}}$introduces many units as part
of the translation (e.g., $|u:\phi\Rightarrow A|=\mathbf{1}\to|A|$). This is
necessary to ensure the property that no well-typed term can signal an error.
Consider the example:

$\hat{\lambda}||u:\bot||.\mathsf{absurd}(u):(u:\bot)\Rightarrow A$

This erases to the term:

$\lambda x:\mathbf{1}.\mathsf{error}$

Without the $\lambda x:\mathbf{1}$, the term would erase to $\mathsf{error}$,
which violates our invariant.

It is possible to avoid introducing any units at all if the base calculus is
in call-by-push-value form. However, since one of our main objectives was to
have a simple, familiar semantics, we the price of introducing units was lower
than introducing call-by-push-value.

##### Automation and Solver Integration

One of the critical advantages of refinement types is the potential for
significantly reducing the annotation burden of formal verification. Hence, to
make $\lambda_{\mathsf{ert}}$ usable, it should be able to be automated to a
similar degree for similarly complex programs. One potential form of basic
automation is support for an ”$\mathsf{smt}$” tactic, similar to section 3’s
”$\beta$” tactic; we can similarly envision calling out to various automated
theorem provers like Vampire (Kovács and Voronkov, 2013) or SPASS (Weidenbach
et al., 2002).

A more powerful approach would be to adapt the work on Liquid Typing (Rondon
et al., 2008) to this setting, which works by inferring appropriate refinement
types and proofs for an unrefined program such that, given that the program’s
preconditions are satisfied, the preconditions of all function calls within
the program as well as the postconditions of the program are both satisfied.
Liquid Typing sometimes requires annotations to infer appropriate invariants
and may require explicit checks to be added for conditions it cannot verify
are implied by the preconditions. One way to combine Liquid Typing with
$\lambda_{\mathsf{ert}}$ would be to, using $\lambda_{\mathsf{ert}}$ types as
annotations, automatically refine the types of subterms of an
$\lambda_{\mathsf{ert}}$ program to make it typecheck, inferring and inserting
proofs as necessary. One advantage of this approach would be that (assuming it
compiles down to fully-annotated $\lambda_{\mathsf{ert}}$) it removes the
liquid typing algorithm itself from the trusted codebase, and, if the solvers
used support proof output, the solvers themselves as well. Furthermore, we
could replace potentially expensive runtime checks with explicit proofs.

##  8\. Related Work

###  8.1. Relationship of $\lambda_{\mathsf{ert}}$ to Dependent Types

The most well-known approach to designing programming languages with
integrated support for proof is dependent type theory. The semantics of
dependent type theories is generally given in an ”intrinsic” style, in which
well-typed terms (in fact, typing derivations) are given a denotational
semantics, and ill-typed terms are regarded as meaningless (i.e., have no
semantics).

On the other hand, $\lambda_{\mathsf{ert}}$ is a refinement type system, which
takes an existing programming language (in this case, the simply-typed lambda
calculus with error stops), and extends it so that existing programs can be
given richer, more precise types. This ensures that it is always possible to
forget the rich types and be left with the simply-typed skeleton. A good
analogy is to Hoare logic, in which pre-conditions, post-conditions and loop
invariants can be seen as rich type annotations on a simple while-program.
These logical annotations can always be erased, leaving behind an untyped
while-program.

Like in Hoare logic, $\lambda_{\mathsf{ert}}$ distinguishes logical assertions
from the type-theoretic structure of the programming language. This is in
contrast to the traditional Curry-Howard interpretation of logic in dependent
type theory, and more closely resembles the $\mathsf{Prop}$ type of Coq (which
is a sort of purely logical assertions), or even more closely the ”logic-
enriched type theories” of Aczel and Gambino (Gambino and Aczel, 2006) (which
extends type theory with a new judgement of logical propositions).

Most dependent type theories also feature a notion of judgemental equality, in
which types are considered equal modulo some equational theory (usually
containing $\beta$ and sometimes $\eta$-conversions). $\lambda_{\mathsf{ert}}$
is designed to work without a judgemental equality, since it is a source of
both metatheoretical difficulty, and complicates the design of tooling.
However, there are some dependent type theories, such as Objective Type Theory
(van den Berg and den Besten, 2021) and Zombie (Sjöberg and Weirich, 2015),
which implement reduction propositionally as axioms, similarly to what we have
done.

###  8.2. Refinement Logics and Squashed Curry-Howard

As is well-known, even type theories without a $\mathsf{Prop}$ sort like Coq
or Lean’s still have a logical reading – the famous ”propositions as types”
principle, where each type-theoretic connective (function types, pairs, sums)
corresponds to a logical connective (implication, conjunction, disjunction).

This is unsuitable for our purposes. We plan to use $\lambda_{\mathsf{ert}}$
as the basis of extending practical SMT-based refinement type systems with
explicit proofs, and SMT solvers are fundamentally based on classical logic.
So we want the semantics of the propositions in our refinement types to be
classical as well, which is not possible when propositions and types are
identified.

This also makes it difficult to use the various modal techniques proposed to
integrate proof irrelevance into type theory, such as Awodey and Bauer’s
squash types (Awodey and Bauer, 2004), or Sterling and Harper’s phase
modalities (Sterling and Harper, 2021).

For example, with the Awodey-Bauer squash type $[A]$, logical disjunctions and
existentials are encoded as

(26) $\begin{array}[]{l}P\vee Q=[P+Q]\\\ \exists x:X.P\,=[\Sigma
x:X.P]\end{array}$

where the $[-]$ operator has a degenerate equality. As a result, if the type
theory is intuitionistic the logic of propositions must be as well, which is
contrary to our needs.

However, there is a deeper problem with using squash types. The semantics of
the Awodey-Bauer squash type is such that if $P$ is a proposition (i.e., all
inhabitants are equal), then $P$ and $[P]$ are isomorphic. Since $P$ is a
proposition if all its inhabitants are equal, a contractible type like $\Sigma
x:\mathbb{N}.\,x=n$ is a proposition, and hence there is a map $[\Sigma
x:\mathbb{N}.x=n]\to\Sigma x:\mathbb{N}.x=n$.

That is, it is possible to extract computational data from a squashed type,
and so erasure of propositions and squashed types is a much more subtle
problem than it may first seem. Kraus et al’s paper Notions of Anonymous
Existence in Martin-Löf Type Theory (Kraus et al., 2017) studies this and
similar issues in detail. There is a similar obstacle when using the Sterling-
Harper approach, which could use a pair of modalities to control whether a
term is potentially in the specification or runtime phases. Once again, re-
using type-theoretic connectives as logical connectives forces the
identification of the refinement logic and the type theory.

###  8.3. Erasure in Dependent Type Theory

Coq (The Coq Development Team, 2021) supports a notion of erasure, in which
terms of proposition type are systematically elided as a dependently-typed
program is extracted to a functional language like Ocaml or Haskell. It also
lets users declare certain function parameters as useless, but since Coq does
not distinguish logical variables from computational ones in its type system,
a well-typed Coq term may fail to successfully extract. In contrast,
$\lambda_{\mathsf{ert}}$ can always erase both proofs and logical variables,
and furthemore guarantees that all erased terms are also well-typed because it
is a refinement over a pre-existing simple type theory. This is not the case
in Coq, where extracted terms may have to use the unsafe cast
$\mathsf{Obj.magic}$.

Another critical feature of $\lambda_{\mathsf{ert}}$ is that it supports
Hoare-style logical variables. is that they are not program variables, and
cannot influence the runtime behaviour of a program – they only exist for
specification purposes. So in a type

(27) $\mathsf{vlen}:\forall n:\mathbb{N}.\mathsf{Vec}\;n\to\\{x:\mathbb{N}\mid
x=n\\}$

where $\forall n:\mathbb{N}$ is an intersection-style quantifier, it is only
possible to compute the length of the list by actually traversing the list. In
plain Martin Löf type theory, the corresponding type has a degenerate
implementation:

(28) $\begin{array}[]{l}\mathsf{vlen}:\Pi
n:\mathbb{N}.\mathsf{Vec}\;n\to\Sigma x:\mathbb{N}.x=n\\\
\mathsf{vlen}\;n\;\\_\equiv(n,\mathsf{refl})\end{array}$

This kind of computational irrelevance is different from what is sometimes
called proof-irrelevance or definitional irrelevance, since different values
of $n$ are not equal.

Two approaches that have arisen to manage this kind of irrelevance are the
implicit forall quantifier of the implicit calculus of constructions (ICC)
(Barras and Bernardo, 2008), and the usage annotations in Atkey and McBride’s
quantitative type theory (QTT) (Atkey, 2018).

As we did, the ICC introduced an intersection type $\forall x:T.U$ to support
computationally irrelevant quantification. However, because there was no
separation of the refinement layer from the base layer, the denotational
semantics of the ICC is much more complicated – the Luo-style extended
calculus of constructions (ECC) (Luo, 1990) has a simple set-theoretic model,
but the only known denotational model of the ICC (Miquel, 2000) is based on
coherence spaces. In our view, this is a significant increase in the
complexity of the model.

In contrast, we are able to model intersection types with ordinary set-
theoretic intersections. The reason for this is that the refinement type
discipline ensures that we only ever make use of _structural_ set-theoretic
operations. That is, every $\lambda_{\mathsf{ert}}$ type is a subset of an
underlying base type, and so when we take an intersection, we are only taking
the intersection of a family of subsets of a particular set (the base type).
From a mathematical point of view, this is much better-behaved than taking
intersections of _arbitrary_ sets, and having this invariant lets us interpret
intersections more simply than is possible in the semantics of the ICC.

Our semantics (and indeed, syntax) for intersection types is very similar to
the semantics of the ”dependent intersection types” introduced by Kopylov
(2003) for the Nuprl system. They worked with partial equivalence relations
over a term model, rather than our simple set-theoretic model. As mentioned
above, we will also need to move to a PER model to support function
extensionality, though we expect we can still consider PERs over sets, rather
than having to use a term model.

In his PhD dissertation (Tejiščák, 2019), Tejiščák studies how to apply QTT
directly to the problem of managing computational irrelevance. The runtime and
erasable annotations in QTT look very similar to our distinction between
computational and ghost variables. However, we cannot directly use this type
system, because it does not have a sort of propositions, and therefore must
express logical properties in a construtive, Curry-Howard logic.

###  8.4. Relation to Other Systems

ATS (Cui et al., 2005) is a system in the Dependent ML style. That is, the
type system has a very hard separation between indices (which can occur inside
types) and terms (which do runtime computation). Like
${\lambda_{\mathsf{ert}}}$, it is possible in ATS to give explicit proofs of
quantified and inductive formulae.

ATS’s erasure theorem is proved operationally, by exhibiting a simulation
between the reductions of the fully-typed language and erased, untyped
programs. This makes it hard to reason about the equality of program terms
(something like a logical relation would have to be added), but ATS does not
have to, because it distinguishes program terms and indices, and only permits
indices to occur in types.

However, since program terms cannot occur in constraints, correctness
arguments about functions are forced into an indirect style – for each
recursive function, one must define an inductive relation encoding its graph,
and then show that inputs and outputs are related according to this relation.
As a result, proving something like (e.g.) that the type of endofunctions
$A\to A$, the identity, and function composition have the structure of a
monoid will be very challenging. In ${\lambda_{\mathsf{ert}}}$, in contrast,
this would be very straightforward, since (following liquid types) indices and
program terms are one and the same.

Modern ATS has also extended the proposition language to support a notion of
linear assertion, which permits verifying imperative programs in the style of
separation logic. Extending ${\lambda_{\mathsf{ert}}}$ with support for richer
reasoning about effectful programs is ongoing work.

$\mathrm{F}^{\ast}$is a full dependent type theory which has replaced the
usual conversion relation with an SMT-based approach. $\mathrm{F}^{\ast}$makes
no effort to keep quantifiers out of the constraints sent to its SMT solver,
and hence does not (and cannot) have any decidability guarantees – the
$\mathrm{F}^{\ast}$typechecking problem is undecidable. This best-effort view
lets $\mathrm{F}^{\ast}$take maximum advantage of the solver, at the price of
sometimes letting the typechecker loop. In contrast,
${\lambda_{\mathsf{ert}}}$ has decidable, near linear-time typechecking,
because typing is fully syntax-directed and has no conversion relation.

The treatment of computational irrelevance in $\mathrm{F}^{\ast}$is similar in
effect (though different in technical detail) to ICC. As in ICC, ghost
arguments can affect typing but not computations, but there is no notion of a
less-typed base language that ghosts can be erased to.

## References

  * (1)
  * Ahman (2018) Danel Ahman. 2018\.  Handling fibred algebraic effects.  _Proc. ACM Program. Lang._ 2, POPL (2018), 7:1–7:29.  https://doi.org/10.1145/3158095
  * Atkey (2018) Robert Atkey. 2018\.  The Syntax and Semantics of Quantitative Type Theory. In _LICS ’18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9–12, 2018, Oxford, United Kingdom_.  https://doi.org/10.1145/3209108.3209189
  * Awodey and Bauer (2004) Steven Awodey and Andrej Bauer. 2004.  Propositions as [types].  _Journal of logic and computation_ 14, 4 (2004), 447–471.
  * Barras and Bernardo (2008) Bruno Barras and Bruno Bernardo. 2008.  The implicit calculus of constructions as a programming language with dependent types. In _Foundations of Software Science and Computational Structures: 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 11_. Springer, 365–379.
  * Cui et al. (2005) Sa Cui, Kevin Donnelly, and Hongwei Xi. 2005.  Ats: A language that combines programming with theorem proving. In _Frontiers of Combining Systems: 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005. Proceedings 5_. Springer, 310–320.
  * Gambino and Aczel (2006) Nicola Gambino and Peter Aczel. 2006.  The generalised type-theoretic interpretation of constructive set theory.  _The Journal of Symbolic Logic_ 71, 1 (2006), 67–103.  https://doi.org/10.2178/jsl/1140641163
  * Harper (1992) Robert Harper. 1992\.  Constructing type systems over an operational semantics.  _Journal of Symbolic Computation_ 14, 1 (1992), 71–84.  https://doi.org/10.1016/0747-7171(92)90026-Z
  * Jhala and Vazou (2020) Ranjit Jhala and Niki Vazou. 2020.  Refinement Types: A Tutorial.  _arXiv e-prints_ , Article arXiv:2010.07763 (Oct. 2020), arXiv:2010.07763 pages.  arXiv:2010.07763 [cs.PL]
  * Katsumata (2014) Shin-ya Katsumata. 2014\.  Parametric Effect Monads and Semantics of Effect Systems. In _Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Diego, California, USA) _(POPL ’14)_. Association for Computing Machinery, New York, NY, USA, 633–645.  https://doi.org/10.1145/2535838.2535846
  * Kopylov (2003) Alexei Kopylov. 2003\.  Dependent Intersection: A New Way of Defining Records in Type Theory. In _18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings_. IEEE Computer Society, 86–95.  https://doi.org/10.1109/LICS.2003.1210048
  * Kovács and Voronkov (2013) Laura Kovács and Andrei Voronkov. 2013.  First-Order Theorem Proving and Vampire. In _Computer Aided Verification_ , Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–35.
  * Kraus et al. (2017) Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. 2017.  Notions of anonymous existence in Martin-Löf type theory.  _Logical Methods in Computer Science_ 13, 1 (2017).
  * Kura (2021) Satoshi Kura. 2021\.  A General Semantic Construction of Dependent Refinement Type Systems, Categorically. In _Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings_ _(Lecture Notes in Computer Science, Vol. 12650)_ , Stefan Kiefer and Christine Tasson (Eds.). Springer, 406–426.  https://doi.org/10.1007/978-3-030-71995-1_21
  * Luo (1990) Zhaohui Luo. 1990\.  _An extended calculus of constructions_.  Ph. D. Dissertation. University of Edinburgh.
  * Melliès and Zeilberger (2015) Paul-André Melliès and Noam Zeilberger. 2015.  Functors Are Type Refinement Systems. In _Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Mumbai, India) _(POPL ’15)_. Association for Computing Machinery, New York, NY, USA, 3–16.  https://doi.org/10.1145/2676726.2676970
  * Milner (1978) Robin Milner. 1978\.  A theory of type polymorphism in programming.  _Journal of computer and system sciences_ 17, 3 (1978), 348–375.
  * Miquel (2000) Alexandre Miquel. 2000\.  A model for impredicative type systems, universes, intersection types and subtyping. In _Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332)_. IEEE, 18–29.
  * Moggi (1991) Eugenio Moggi. 1991\.  Notions of computation and monads.  _Information and Computation_ 93, 1 (1991), 55–92.  https://doi.org/10.1016/0890-5401(91)90052-4 Selections from 1989 IEEE Symposium on Logic in Computer Science.
  * Reynolds (2003) John C. Reynolds. 2003\.  _What do types mean? — From intrinsic to extrinsic semantics_.  Springer New York, New York, NY, 309–327.  https://doi.org/10.1007/978-0-387-21798-7_15
  * Rondon et al. (2008) Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008\.  Liquid Types.  _SIGPLAN Not._ 43, 6 (jun 2008), 159–169.  https://doi.org/10.1145/1379022.1375602
  * Sjöberg and Weirich (2015) Vilhelm Sjöberg and Stephanie Weirich. 2015.  Programming up to Congruence.  _SIGPLAN Not._ 50, 1 (Jan. 2015), 369–382.  https://doi.org/10.1145/2775051.2676974
  * Sterling and Harper (2021) Jonathan Sterling and Robert Harper. 2021.  Logical relations as types: Proof-relevant parametricity for program modules.  _Journal of the ACM (JACM)_ 68, 6 (2021), 1–47.
  * Tejiščák (2019) Matúš Tejiščák. 2019\.  _Erasure in Dependently Typed Programming_.  Ph. D. Dissertation. University of St. Andrews.
  * The Coq Development Team (2021) The Coq Development Team. 2021\.  _The Coq Proof Assistant_.  LogiCal Project.  https://doi.org/10.5281/zenodo.4501022
  * van den Berg and den Besten (2021) Benno van den Berg and Martijn den Besten. 2021.  Quadratic type checking for objective type theory.  _arXiv e-prints_ , Article arXiv:2102.00905 (Feb. 2021), arXiv:2102.00905 pages.  arXiv:2102.00905 [cs.LO]
  * Vazou and Greenberg (2022) Niki Vazou and Michael Greenberg. 2022.  How to safely use extensionality in Liquid Haskell. In _Haskell ’22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022_ , Nadia Polikarpova (Ed.). ACM, 13–26.  https://doi.org/10.1145/3546189.3549919
  * Vazou et al. (2014) Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014\.  Refinement Types for Haskell.  _SIGPLAN Not._ 49, 9 (aug 2014), 269–282.  https://doi.org/10.1145/2692915.2628161
  * Weidenbach et al. (2002) Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobald, and Dalibor Topić. 2002.  Spass Version 2.0. In _Automated Deduction—CADE-18_ , Andrei Voronkov (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 275–279.
  * Winterer et al. (2020) Dominik Winterer, Chengyu Zhang, and Zhendong Su. 2020\.  On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers.  4, OOPSLA, Article 193 (nov 2020), 25 pages.  https://doi.org/10.1145/3428261
  * Xi and Pfenning (1998) Hongwei Xi and Frank Pfenning. 1998.  Eliminating Array Bound Checking through Dependent Types. In _Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation_ (Montreal, Quebec, Canada) _(PLDI ’98)_. Association for Computing Machinery, New York, NY, USA, 249–257.  https://doi.org/10.1145/277650.277732

##  Appendix A Appendix

¡A, B, C¿ ::= $\mathbf{1}$ (¡x¿ ”:” ¡A¿) ”$\to$” ¡B¿ (¡x¿ ”:” ¡A¿) ”$\times$”
¡B¿ ¡A¿ ”+” ¡B¿ $({u}:{\varphi})\Rightarrow{A}$
$\left\\{{x}:{A}\mid{\varphi}\right\\}$ ”$\forall$” ¡x¿ ”:” ¡A¿, ¡B¿
”$\exists$” ¡x¿ ”:” ¡A¿, ¡B¿ $\mathbb{N}$ $\lambda_{\mathsf{ert}}$ types

(a) $\lambda_{\mathsf{ert}}$ types

¡$\varphi$, $\psi$, $\phi$¿ ::= $\top$ $\bot$
$({u}:{\varphi})\Rightarrow{\psi}$ (¡u¿ ”:” ¡$\varphi$¿) ”$\land$” ¡$\psi$¿
¡$\varphi$¿ ”$\lor$” ¡$\psi$¿ ”$\forall$” ¡u¿ ”:” ¡A¿, ¡$\varphi$¿ ”$\exists$”
¡u¿ ”:” ¡A¿, ¡$\varphi$¿ ¡a¿ $=_{A}$ ¡b¿ $\lambda_{\mathsf{ert}}$ propositions

(b) $\lambda_{\mathsf{ert}}$ propositions

¡a, b, c, e, e’¿ ::= $()$ ¡x, y, z¿ $\lambda$ ¡x¿ ”:” ¡A¿, ¡e¿ ¡a¿ ¡b¿ $(a,b)$
$\mathsf{let}$ $(x,y)$ ”:” ¡A¿ ”=” ¡e¿ $\mathsf{in}$ ¡e’¿ $\mathsf{inl}$ ¡e¿
$\mathsf{inr}$ ¡e¿ $\mathsf{cases}$ [¡x¿ $\mapsto$ ¡C¿] ¡e¿ ($\mathsf{inl}$
¡y¿ ”$\mapsto$” ¡a¿) ($\mathsf{inr}$ ¡z¿ ”$\mapsto$” ¡b¿) $\lambda$ ¡x¿ ”:”
¡$\varphi$¿, ¡e¿ ¡a¿ ¡p¿ $\\{a,p\\}$ $\mathsf{let}$ $\\{x,u\\}$ ”:” ¡A¿ ”=”
¡e¿ $\mathsf{in}$ ¡e’¿ $\lambda$ $\|x:A\|$, ¡e¿ ¡a¿ $\|b\|$ ($\|$ ¡a¿ $\|$,
¡b¿) $\mathsf{let}$ $(\|x\|,y)$ ”:” ¡A¿ ”=” ¡e¿ $\mathsf{in}$ ¡e’¿ $0$
$\mathsf{succ}$ $\mathsf{natrec}$ [¡x¿ $\mapsto$ ¡C¿] ¡e¿ ¡a¿
($\|$$\mathsf{succ}$ ¡y¿$\|$, ¡z¿ $\mapsto$ ¡b¿) $\mathsf{absurd}$ ¡p¿
$\lambda_{\mathsf{ert}}$ terms

(c) $\lambda_{\mathsf{ert}}$ terms

¡p, q, r¿ ::= $\langle\rangle$ ¡u, v, w¿ $\mathsf{absurd}$ ¡p¿
$\hat{\lambda}x:\varphi$, ¡p¿ ¡p¿ ¡q¿ $\langle p,q\rangle$ $\mathsf{let}$
$\langle x,y\rangle$ ”:” ¡$\varphi$¿ ”=” ¡p¿ $\mathsf{in}$ ¡q¿ $\mathsf{orl}$
¡p¿ $\mathsf{orr}$ ¡q¿ $\mathsf{cases}_{\mathsf{or}}$ [¡u¿ $\mapsto$ ¡$\phi$¿]
¡p¿ ($\mathsf{orl}$ ¡y¿ $\mapsto$ ¡q¿) ($\mathsf{orr}$ ¡z¿ $\mapsto$ ¡r¿)
$\hat{\lambda}$ $\|$ ¡x¿ ”:” ¡A¿ $\|$, ¡p¿ ¡p¿ $\|a\|$ $\langle\|a\|,p\rangle$
$\mathsf{let}$ $\langle\|x\|,u\rangle$ ”:” ¡$\varphi$¿ ”=” ¡p¿ $\mathsf{in}$
¡q¿ $\mathsf{let}$ $(x,y)$ ”:” ¡A¿ ”=” ¡p¿ $\mathsf{in}$ ¡q¿ $\mathsf{let}$
$\\{x,y\\}$ ”:” ¡A¿ ”=” ¡p¿ $\mathsf{in}$ ¡q¿ $\mathsf{let}$ $(\|x\|,u)$ ”:”
¡A¿ ”=” ¡p¿ $\mathsf{in}$ ¡q¿ $\mathsf{subst}$[¡x¿ $\mapsto$ ¡B¿][¡a¿ $\to$
¡b¿] ¡p¿ ¡q¿ $\mathsf{cases}$ [¡x¿ $\mapsto$ ¡$\varphi$¿] ($\mathsf{inl}$ ¡y¿
”$\mapsto$” ¡p¿) ($\mathsf{inr}$ ¡z¿ ”$\mapsto$” ¡q¿) $\mathsf{ind}$ [¡x¿
$\mapsto$ ¡$\varphi$¿] ¡e¿ ¡p¿ ($\mathsf{succ}$ ¡y¿, ¡u¿ $\mapsto$ ¡q¿)
¡axiom¿ $\lambda_{\mathsf{ert}}$ proofs

(d) $\lambda_{\mathsf{ert}}$ proofs

¡axiom¿ ::= $\mathsf{rfl}$ ¡a¿ $\mathsf{discr}$ ¡a¿ ¡b¿ ¡p¿ $\mathsf{uniq}$
¡a¿ ¡beta¿ $\eta_{\mathsf{ty}}$ ¡e¿ $\mathsf{ext}_{\mathsf{ty}}$ ¡f¿ ¡g¿ ¡i¿
¡p¿ $\mathsf{ext}_{\mathsf{pr}}$ ¡f¿ ¡g¿ ¡i¿ ¡p¿ $\mathsf{ir}_{\mathsf{pr}}$
[¡x¿ $\mapsto$ ¡e¿] ¡p¿ ¡q¿ $\mathsf{ir}_{\mathsf{ty}}$ ¡e¿ ¡a¿ ¡b¿

(e) $\lambda_{\mathsf{ert}}$ axioms

¡beta¿ ::= $\beta_{\mathsf{pr}}$ (¡x¿ $\mapsto$ ¡e¿) ¡p¿ $\beta_{\mathsf{ty}}$