This paper addresses (part of) the problem of simplifying reasoning with proof assistants by transferring theorems that are stated in a heavy form, using explicit invariants, to lightweight counterparts where the invariants are handled implicitly by the type system. Specifically, we provide some abstract assumptions that allow one to establish isomorphisms for nested applications of defined types in Gordon's Higher-Order Logic (HOL). This allows the seamless isomorphic transfer of results across type definitions in the presence of nesting. Our results have been formalized in the Isabelle/HOL theorem prover, and we plan to integrate them with Isabelle's Lifting and Transfer tool.
theorem provers, including HOL4 [
Namely, say one has a type (perhaps an algebraic datatype) that does not capture precisely the intended concept (because it contains too many elements), but only via an invariant defined in terms of a predicate on , or equivalently, a set that has type set.1 Then one defines the more precise type as a typedef, to consist of exactly the inhabitants of that belong to the set —i.e., is efectively turned
Let us consider two examples, which will act as our running examples throughout this paper. Example 1. (Distinct Lists) Polymorphic lists are introduced as the following datatype, where we use ML-style notation feature by Isabelle/HOL as well as all the HOL-based provers (in particular, denotes a type variable):
datatype list = Nil ∣ Cons ( list) For a list xs, we let length xs be its length and, given a natural number < length, we let xs! be the (−1) ’th element in xs (so the indexing starts from 0). In some developments, one may be interested in working with nonrepetitive (“distinct”) lists, i.e., lists whose elements do not repeat—to this end, one defines the (polymorphic) predicate distinct ∶ list → bool by distinct xs ≡ ∀ . < ∧ < length xs ⟶ xs! ≠ xs! .
The new (polymorphic) type dlist of distinct lists is defined as a typedef:
typedef dlist = {xs ∶ list ∣ distinct xs}
This command introduces the new type dlist together with an abstraction-representation pair of (polymorphic) constants2 (Repdlist, Absdlist) with Repdlist ∶ dlist → list and Absdlist ∶ list → dlist
0 or defined functions, are called “constants”; they are to be contrasted with “variables”, which do not have a fixed interpretation but range over given types. CEUR
ceur-ws.org and the following axioms stating that these functions are mutually inverse bijections between the new type dlist and the subset {xs ∶ list ∣ distinct xs} of the base type list.3 In Isabelle/HOL, these axioms are actually packed into a single axiom:
type_definition Rep dlist Absdlist {xs ∶ list ∣ distinct xs} where the (polymorphic) predicate type_definition ∶ ( → ) → ( → ) → ( follows: type_definition ≡ (∀. ∈ ) ∧ (∀ ∶ . ( ) = ) ∧ (∀ ∶ . ∈ ⟶ ( ) = )
Thus, in this example is list, is {xs ∶ list ∣ distinct xs}, and is dlist. set) → bool is defined as □ .
Example 2. (Discrete Distributions) A (discrete) distribution is a positive function to the real numbers of countable support such that its values sum up to to 1. The polymorphic type distrib of distributions on is introduced as a typedef having base type → real (the type of functions from to real ): typedef distrib = { ∶ → real ∣ dist xs} where the predicate dist ∶ ( → real) → bool is defined by dist ≡ (∀ ∶ . ≥ 0) ∧ countable { ∶ ∣ ≠ 0} ∧ ∑∶ = 1 .
As before, the above command introduces a new type distrib , an abstraction-representation pair of constants (Repdlist, Absdlist) with (Repdistrib, Absdistrib) with Repdistrib ∶ distrib → list, and the axiom type_definition Rep distrib Absdistrib { ∶ → real ∣ dist } saying that Absdistrib and Repdistrib are mutually inverse bijections between distrib and { ∶ → real ∣ distrib xs}.
Thus, in this example is → real, is { ∶ → real ∣ dist xs}, and is distrib. □
In a formal development that follows the above scheme, one usually distinguishes between:
• developing the “internal” mathematical theory, which usually proceeds without defining , but
instead working with and stating the theorems relativized to —for example, proving facts of
the form ∀ ∶ . ∈ ⟶ . . .
• at the end, defining and “sealing” the library for export by transferring from to all the
constants and all the main (exportable) facts that have been proved proved relative to —for
example, turning facts of the form ∀ ∶ . ∈ ⟶ . . . into facts of the form ∀ ′ ∶ . . . .
The process of “isomorphically” transferring -relativized constants and results on to corresponding
constants and results on , while seemingly conceptually straightforward, turns out to be quite subtle
in the presence of higher-order constants. It requires infrastructure for lifting relations along type
constructors (known as relators), which allows the automated proofs of the transferred theorems from
the original ones—this is facilitated in Isabelle/HOL by various dedicated tools [
In this short work-in-progress paper, we study a fairly common pattern: the isomorphic transfer in
the presence of nested type constructors. We start with motivation in terms of a standard construction
applied to our running examples (§2), which leads to formulating the wider scope of the problem. We
then work out the solution to the problem in an ad hoc manner on the running examples §3. After that,
we are ready to describe our main result: some abstract general structure and conditions that enable
this pattern, in that they allow constructing a back-and-forth bijection for transfer (§4), and show how
it instantiates to our examples. We conclude with related work and future plans, notably the planned
integration of our work into Isabelle’s Lifting and Transfer package (§ 5). Our concepts and results apply
to Higher-Order Logic, hence are in principle relevant to any HOL-based provers. We have formalized
them in the Isabelle/HOL theorem prover, and the formal scripts are publicly available [
Consider the problem of proving that the type constructors (polymorphic types) dlist and distrib
constitute monads [
According to the above pattern, one wishes to first prove the properties for the underlying (representing types) list and → real relative to the defining predicates distinct and dist, and then transfer them to the defined types dlist and distrib. (Not only is this good practice, but in some sense it is the only way to proceed, at least initially when “bootstrapping” a theory for the defined types, given that initially our only means to prove a property on the defined type is to trace it back to a property on the underlying type.)
Some of the monadic structure and properties involve nesting the application of type constructors, for example we want to have a map (functorial-action) operator mapdistrib ∶ ( → ) → ( distrib → distrib) and join (counit) operator joindistrib ∶ ( distrib) distrib → distrib satisfying (among others) the associativity law joindistrib ∘ (mapdistrib joindistrib) = joindistrib ∘ joindistrib.
How to define such structure and prove such properties on the defined types? Let us start with a simple example that does not involve nesting, namely defining the map operator on ( → ) → ( distrib → distrib) and proving that it preserves identities, in that ∀ ∶ distrib. mapdistrib (id ∶ → ) = where id denotes the identity function. We define mapdistrib on any ∶ → and ∶ distrib by mapdistrib = Absdistrib ( ∶ . ∑∈ −1 Repdistrib ) . Notice that the definition requires a backand-forth application of the abstraction and representation functions Absdistrib and Repdistrib, with some specific manipulation of items of the underlying type → real. (In this case, the specific manipulation happens to involve taking the sum of a function in → real over all the elements of the -preimage of , but the exact nature of such manipulations is not important here.) Now, to prove the desired fact, ifx ∶ distrib. In order to show mapdistrib id = , by the injectivity of Repdistrib it sufixes to show Repdistrib (mapdistrib id ) = Repdistrib . Using the definition of mapdistrib and the fact that Repdistrib is left-inverse to Absdistrib, the above is equivalent to ∶ . ∑∈ id−1 Repdistrib = Repdistrib , i.e., to ∶ . ∑= Repdistrib = Repdistrib , which follows from the properties of sums and function extensionality.
We thus have the following pattern: To define constants on the defined type and prove properties for them, we need to move back and forth via the abstraction-representation pair and use consequences of the associated type_definition axiom.
But how to do this in the presence of nested defined type constructors (where the abstractionrepresentation pairs stemming from type definitions no longer work out of the box)? In the next section, we discuss in an ad hoc manner how to tackle the nested isomorphic transfer problem in the presence of nested types for our two running examples. After that, we will introduce an abstract solution, which covers these two cases and many others.
Now let us come back to the original more complex problem, of defining joindistrib ∶ ( distrib) distrib → distrib (in addition to mapdistrib which we have already defined) and proving the associativity law.
In order to define joindistrib , which operates on the nested defined type ( distrib) distrib, we need an understanding of how a counterpart of this operator should act on the (nested application of) the underlying type, i.e., on ( → real)real. To be more exact, we don’t need to consider the behavior of such a counterpart on all functions ∶ ( → real) → real, but seemingly only on functions that act like distributions, i.e., satisfy distrib (i.e., are positive, have countable support and sum to 1). In fact, upon a closer look we see that the functions of interest are not really distributions on the entire type → real, but on the subset of → real that consists of distributions only, i.e., distributions on the set { ∶ → real ∣ distrib } . In other words, we need a relativized version of the predicate distrib, let us denote it by distOn ∶ set → distrib → bool, defined by distOn ≡ (∀ ∶ .
∈ ⟶ ≥ 0) ∧ countable { ∶ ∣ ∈ ∧ ≠ 0} ∧ ∑ ∈ = 1 where we have highlighted the diference from the original predicate dist—in that the conditions are not applied to the entire type , but to a parameter subset ∶ set. Note that we can recover the original predicate as dist = distOn UNIV, where UNIV is the “universal” set covering the entire type.
With this relativized predicate at hand, the picture becomes clear: Given a function ∶ ( → real) → real that acts like a distribution on distributions on , i.e., such that distOn { ∶ → real ∣ dist } holds, we have the formal means to turn it into a “flat” distribution, let us call it join , on → real, namely by summation (applying of course a well-known mathematical construction): join ≡ ∑ ∈{ ∣ dist } . Now, to define joindistrib from join, we need to able to move back and forth between distrib distrib and and ( → real) → real, ideally using a similar infrastructure as the abstraction-representation pair (Absdistrib, Repdistrib) and predicate distrib that allowed us to move between distrib and → real. And indeed, this is possible: • We define dist2 ∶ (( → real) → real) → bool to be distOn { ∶ → • We define Absdistrib,2 ∶ (( → real) → real) → ( distrib) distrib by
Absdistrib,2 = Absdistrib ( ∶ distrib. ( Repdistrib )) . • We define Repdistrib,2 ∶ ( distrib) distrib → (( → real) → real) by
Repdistrib,2 = ∶ → real. Repdistrib ( Absdistrib ) . real ∣ dist } .
Note that we defined distrib2 in line with the above analysis, and defined Absdistrib,2 and Repdistrib,2 with the aim of achieving a bijective correspondence between ( distrib) distrib and the elements of ( → real) → real satisfyig dist2. Therefore, we can prove that type_definition Abs distrib,2 Repdistrib,2 { ∣ dist2 } holds.
It now remains to prove the associativity of joindistrib, which we can rephrase as ∀ ∶ ((
distrib) distrib) distrib. joindistrib (mapdistrib joindistrib ) = joindistrib (joindistrib ) .
This involves further level of nesting of distrib; to this end, by essentially iterating one more step the above construction, we obtain dist3 ∶ ((( → real) → real) → real) → bool , Absdistrib,3 ∶ ((( → real) → real) → real) → (( distrib) distrib) distrib and Repdistrib,3 ∶ (( distrib) distrib) distrib → ((( → real) → real) → real) such that type_definition Abs distrib,3 Repdistrib,3 { ∣ dist3 } holds. Now we can easily prove associativity similarly to how we proceeded in the non-nested case, but using the appropriate back and forth infrastructure in each case, depending on the level of nesting.
A somewhat similar discussion applies to distinct lists, though the details difer: • We define distinct2 ∶ ( list) list → bool by
distinct2 xss ≡ distinct xss ∧ (∀ < length xss. distinct (xss!)) . • We define Absdlist,2 ∶ ( list) list → ( dlist) dlist by
Abslist,2 xss = Abslist (map Abslist xss). • We define Repdlist,2 ∶ ( dlist) dlist → ( list) list by
Replist,2 xss = Replist (map Replist xss). where map is the standard mapping operator for lists. type_definition Abs dlist,2 Repdlist,2 {xss ∣ distinct2 xss} holds.
Again, we have that
With the goal of a general solution in mind, let us note some similarities and commonalities of the above two cases. While for distinct lists the definitions of the one-level-up abstraction and representation functions involve entities of the same kind (namely abstractions for abstractions and representations for representations), in the case of distributions the definitions combine the two, for example the definition of the one-level-up abstraction uses outer abstraction together with inner representation. This is a reflection of lists being a covariant functor and function-space-to-reals being a contravariant functor. The common pattern of the two is, however, the fact that the one-level-up operators employ composition between an (1) operator and (2) the map function for the given functor applied to an operator. This is manifestly clear for distinct lists, for example the one-level-up abstraction Absdlist,2 is the composition of Absdlist with maplist Repdlist; for distributions, this is also seen to be the case, if we note that the map function for the contravariant functor → real is ∶ → . ∶ → real. ∘ .
Another discrepancy between the two cases is the definition of the one-level-up characteristic predicates (distrib2 versus distinct2); as we will see next, we will be able to uniformly capture both cases under a more general set-lifting operator.
We formulate the problem abstractly as follows: How to lift the abstraction-representation properties characteristic of type definitions to nested applications of the defined type constructor? In technical terms: Given a polymorphic type and a polymorphic operator ∶ ( ) set such that ≠ ∅ which produce a type definition
typedef = { ∶ ∣ ∈ } what structure and properties are in general required for and in order to be able to lift the operator and abstraction-representation pair (Abs , Rep ), for any , to -level operator ∶ ( ) set and abstraction-representation pair (Abs, , Rep, ) with Abs, ∶ → and Rep , ∶ → such that type_definition Abs , Rep , { ∶ ∣ } holds? (Above, denotes the ’th iteration of the type constructor , in particular 1 = and 2 = ( ) ; and similarly for .) Indeed, this would allow us to seamlessly apply to the nested case the same back and forth techniques as in the non-nested case.
In the previous section, we have discussed solutions to two instances of this problem. The first instance is representayive of a wide class of situations, namely polymorphic inductive datatypes (which are all covariant functors) with invariants; the second also has some cousins in the formalization and specification literature, for example the defined types topological filters and of mutisets, as well as variations such as discrete subdistributions. In what follows, we introduce a generalization that covers all these cases.
Assumptions. We assume that the underlying type constructor comes equipped with an operator Trel ∶ set → set → ( → → bool) → ( → → bool) for lifting relations to that for bijective relations commutes with composition; namely, letting bijBetw express that the relation is a bijection between and : (A1) bijBetw , , , , and bijBetw implies Trel ( ∘ ) =
Trel ∘
Trel for all
Moreover, we assume that there exists an operator Iset ∶ set → ( ) is an extension of in that set for lifting sets to , which (A2) Iset UNIV = and the following hold, where eqOn diagonal of) :
says that the restriction of to is the equality on (i.e., the
(A3) bijBetw
(A4) bijBetw
implies bijBetw (Iset ) ( Iset ) ( Trel )
and eqOn implies eqOn (Iset ) ( Trel )
for all , ,
for all ,
together with the operator Trel forms a relator-like structure [
Trel and Iset are connected by the assumptions (A3) and (A4). Thus, (A3) states that Trel lifts bijections between two sets to bijections between the Iset-liftings of these sets, which roughly means that Iset partially acts like a subrelator of ( , Trel). Finally, (A4) is an Iset-relativization of the standard property of relators of preserving equalities—namely, here we say Trel preserves partial equalities w.r.t. Iset.
Let us see how to instantiate this framework to our running examples. To this end, we first note that having chosen our assumptions in terms of relations rather than functions allows us to capture both covariant and contravariant cases. For the case of the distribution type distrib, we take: • to be → real; • Trel to be ⇒real (, . ∈ ∧ ∈ ∧ ) ∧ (∀ ∉ . = ⊥) ∧ (∀ ∉ . = ⊥), where ⊥ is a (polymorphic) fixed “undefined” element (which is available in HOL on each type via Hilbert choice) and ⇒real is the real-instance of the function-space relator, defined by ⇒real ≡ ∀, . ⟶ = ; • Iset to be given by the relativized form of the distOn predicate, namely Iset ≡ { ∣ distOn } .
For the case of the distinct-list type dlist, we take: • to be list; • Trel to be the list relator list_all, where list_all relates two lists just in case they have the same length and their elements are position-wise related (thus, the domain and codomain sets are ignored by Trel); • Iset to be defined as Iset ≡ { xs ∣ distinct xs ∧ set xs ⊆ } , where set ∶ list → set is the support operator for lists (returning the set of all elements of a list).
Note the two flavors of instantiating the relativized operator Iset, depending on whether we deal with a contravariant or covariant functor, namely : (1) either, in the contravariant case, by relativizing the original predicate dist to distOn; (2) or, in the covariant case, by intersecting the original predicate distinct with the adjoint of the support operator (which is usually available for covariant functors, and in particular is available for all container types)—indeed, the righthand side of the definition of Iset can be written as {xs ∣ distinct xs} ∩ { ∣ set xs ⊆ } , and the operator = . { ∣ set xs ⊆ } is the right adjoint4 of the support operator set in the sense that xs ∈ if set xs ⊆ . It is relatively easy to check that these instances satisfy our assumptions. For example, (A3) in the case of the distribution instantiation says that a bijection between two sets and induces a bijection the sets of distributions on and respectively, which are constant ⊥ outside and respectively.
Our main result is that these abstract assumptions are suficient for solving our problem, thus generalizing the constructions in the above particular cases (and in many other cases, e.g., any datatypes with invariants turned into typedefs).
Theorem: Under the assumptions (A1)–(A4) above, we have a solution to our problem for all ≥ 1 , in that there exist ∶ ( ) set, Abs, ∶ → and Rep , ∶ → such that type_definition Abs , Rep , holds.
A formal proof in Isabelle/HOL of the core of this theorem can be found in [
Proof sketch. We proceed by induction on . For = 1 , we simply take = , Abs, = Abs and Rep, = Rep , so the desired fact holds by our assumptions.
For the induction step, assume that we have ∶ ( ) set, Abs, ∶ → and Rep , ∶ → such that type_definition Abs , Rep , holds. We define +1 ∶ ( +1 ) set, Abs,+1 ∶ +1 → +1 and Rep ,+1 ∶ +1 → +1 as follows: +1 ≡ Iset ; Abs,+1 = Abs ∘ funOf (Trel (relOf Abs, )); Rep,+1 = Rep ∘ funOf (Trel (relOf Rep, )).
Above, the operators relOf ∶ ( → ) → ( → → bool) and funOf ∶ ( → → bool) → ( → ) provide back and forth conversions between bijective relations and (partially) bijective functins. Namely, we have the following properties for them, where bij_betw says that the restriction of the function ∶ → to ∶ set is a bijection between and ∶ set: (1) If bij_betw , then bijBetw ( relOf ) and funOf (relOf ) = ; (2) If bijBetw , then bij_betw ( funOf ) and relOf (funOf = .
To prove type_definition Abs ,+1 Rep ,+1 +1 compositionally (along the definitions of the abstraction ad represenations operators), we introduce a generalization of type_definition that does not assume one of its argument functions (namely the representation function) to operate on the entire domain, but on an additional parameter set. Namely, we define bij_pair ∶ ( → ) → ( → ) → set → set → bool as follows, where we highlight the diferences from type_definition : bij_pair ≡ (∀ . ∈ ⟶ ∈ ) ∧ (∀. ∈ ⟶ ∈ ) ∧ (∀ ∶ . ∈ ⟶ ( ) = ) ∧ (∀ ∶ . ∈ ⟶ ( ) = ) . Thus, bij_pair says that and are mutually inverse bijections between and ; in particular, we have (3) bij_pair = type_definition UNIV .
Next, we define the relational counterpart of bij_pair, namely bijPair ∶ ( → → bool) → ( → → bool) → set → set → bool, such that bijPair says that and are mutually inverse (relational) bijections between and . The operators bij_pair and bijPair correspond to each other via the translations between functions and relations: (4) If bij_pair then bijPair (relOf ) ( relOf ) ; (5) If bijPair then bij_pair (funOf ) ( funOf ) . They also commute with relation and function composition: (6) If bij_pair and bij_pair ′ ′ then bij_pair ( ′ ∘ ) ( ′ ∘ ) ; (7) If bijPair and bij_pair ′ ′ then bijPair ( ∘ ′) ( ∘ ′) .
Finally, using (A1), (A3) and (A4), we can prove the crucial property that Trel “lifts” the bijPair property relative to Iset: (8) If bijPair then bijPair (Trel ) ( Trel ) ( Iset ) ( Iset ) . □
Note that the theorem asserts the existence of -level predicates and abstraction-representation pairs (Abs , Rep ) which extend the original ones, and (Abs, Rep). But the question arises on whether these are the “right” extensions. The answer relies only on the suitability of , since once that is decided than any projection pair (Abs , Rep ) satisfying type_definition Abs , Rep , would do—mirroring the fact that in a type definition (at level 1) only matters and any (Abs, Rep) satisfying type_definition Abs Rep is as good as any other.
Now, concerning the suitability of , we note from the proof that = Iset UNIV; so it all hinges upon whether Iset is the “right” way of lifting sets of elements of to sets of elements of that respects the intended meaning of the subset of . In other words, whatever concept is supposed to represent, we want that Iset provides a correct relativization of that concept from the entire type to a subset ∶ . Our assumptions (A2)–(A4) are sanity properties for such a relativization, but whether this is the correct relativization needs to be established in each particular case—in other words, it is the responsability of the user of our framework to provide a correct and meaningful Iset operator. This is easily seen to be the case in our two examples, where the move from to Iset clearly represents the move from distributions on the whole type to distributions on a given subset, and from distinct lists on the whole type to distinct lists on a given subset, respectively. Moreover, the scheme that worked for distinct lists (of intersecting with the support operator) works for essentially the same reason for any container type.
Finally, a remark on the generality of the theorem: While we have formulated it in reference to the (possibly iterated) nesting of a single type constructor, the construction and proof can be straightforwardly (albeit tediously) extended to cope with combining / nesting diferent type constructors (which can also have more than one argument).
Isomorphic transfer is an important topic in formal reasoning, and is one of the main motivations of
major recent developments such as Homotopy Type Theory [
Another technical part of our setting concerns the HOL defined types, which are not included in their base types but only injected into them. Other formalisms ofer pure subtyping / inclusion mechanisms, notably PVS [27], F⋆ [28], and logical frameworks featuring refinement types [ 29]—where the goal of isomorphic transfer is replaced by corresponding goals concerning automating aspects of type checking.
Next, we will focus on the most closely related work, namely Isabelle’s Lifting and Transfer package
[
This having been said, our work addresses only a subproblem of the overall lifting and transfer problem, which the Lifting and Transfer package addresses quite comprehensively. So we do not envision our development as an alternative to this mature tool, but as a possible “add-on” that can improve the usability and automation of the tool’s handling of nested types. Since what we produce for nested types are type_definition theorems, these can in principle be directly integrated into the Lifting and Transfer package (via the “setup _lifting” command), save for one dificulty caused by the fact that any provided abstraction operators are currently required to be registered as dataype-like constructors—addressing this formal engineering problem is ongoing work. (Of course, the integration will involve the fully general case, of diferent type constructors of possible multiple arguments nested in arbitrary ways.)
Another short-term plan is to provide some generic infrastructure that automates our inferred result for arbitrary type constructors, which can then be instantiated to diferent cases. This is being tackled (in joint work with Dmitriy Traytel) with the help of a quasi-foundational developement of polymorphic locales, generalizing Isabelle’s standard (monomorphic) locales [31, 32] in a manner that does not impair the meta-properties of the logic and definitional mechanisms underlying Isabelle/HOL [ 33, 34, 35, 36].
Acknowledgments. We thank the three anonymous reviewers for their valuable comments and suggestions, which led to the improvement of the presentation and to the discussion of more related work. CPP, volume 8307 of LNCS, Springer, 2013, pp. 114–130. [21] M. Milehins, An extension of the framework types-to-sets for Isabelle/HOL, in: A. Popescu,
S. Zdancewic (Eds.), CPP 2022, ACM, 2022, pp. 180–196. doi:10.1145/3497775.3503674. [22] G. Barthe, V. Capretta, O. Pons, Setoids in type theory, J. Funct. Program. 13 (2003) 261–293.
doi:10.1017/S0956796802004501. [23] T. Altenkirch, S. Boulier, A. Kaposi, N. Tabareau, Setoid type theory - A syntactic translation, in: G. Hutton (Ed.), Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, volume 11825 of Lecture Notes in Computer Science, Springer, 2019, pp. 155–196. URL: https://doi.org/10.1007/978-3-030-33636-3_7. doi:10.1007/978-3-030-33636-3\_7. [24] Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science. An EATCS Series, Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07964-5. doi:10.1007/ 978-3-662-07964-5. [25] G. Gonthier, A. Mahboubi, An introduction to small scale reflection in coq, J. Formaliz. Reason. 3 (2010) 95–152. URL: https://doi.org/10.6092/issn.1972-5787/1979. doi:10.6092/ISSN.1972-5787/ 1979. [26] L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, J. von Raumer, The lean theorem prover (system description), in: A. P. Felty, A. Middeldorp (Eds.), CADE-25, volume 9195 of LNCS, Springer, 2015, pp. 378–388. doi:10.1007/978-3-319-21401-6\_26. [27] J. M. Rushby, S. Owre, N. Shankar, Subtypes for specifications: Predicate subtyping in PVS, IEEE Trans. Software Eng. 24 (1998) 709–720. URL: https://doi.org/10.1109/32.713327. doi:10.1109/32. 713327. [28] N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P. Strub, M. Kohlweiss, J. K. Zinzindohoue, S. Z. Béguelin, Dependent types and multi-monadic efects in F, in: R. Bodík, R. Majumdar (Eds.), Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, ACM, 2016, pp. 256–270. URL: https://doi.org/10.1145/2837614.2837655. doi:10.1145/2837614.2837655. [29] W. Lovas, F. Pfenning, Refinement types for logical frameworks and their interpretation as proof irrelevance, Log. Methods Comput. Sci. 6 (2010). URL: https://doi.org/10.2168/LMCS-6(4:5)2010. doi:10.2168/LMCS-6(4:5)2010. [30] O. Kunčar, Types, Abstraction and Parametric Polymorphism in Higher-Order Logic, Ph.D. thesis, Fakultät für Informatik, Technische Universität München, 2016. URL: http://www21.in.tum.de/ ~kuncar/documents/kuncar-phdthesis.pdf. [31] F. Kammüller, M. Wenzel, L. C. Paulson, Locales - A sectioning concept for Isabelle, in: Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin-Mohring, L. Théry (Eds.), Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Nice, France, September, 1999, Proceedings, volume 1690 of Lecture Notes in Computer Science, Springer, 1999, pp. 149–166. URL: https://doi. org/10.1007/3-540-48256-3_11. doi:10.1007/3-540-48256-3\_11. [32] C. Ballarin, Locales and locale expressions in isabelle/isar, in: S. Berardi, M. Coppo, F. Damiani (Eds.), Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, volume 3085 of Lecture Notes in Computer Science, Springer, 2003, pp. 34–50. URL: https://doi.org/10.1007/978-3-540-24849-1_3. doi:10.1007/ 978-3-540-24849-1\_3. [33] O. Kuncar, A. Popescu, Comprehending Isabelle/HOL’s consistency, in: H. Yang (Ed.), Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, Springer, 2017, pp. 724–749. URL: https://doi.org/10.1007/978-3-662-54434-1_27. doi:10.1007/ 978-3-662-54434-1\_27. [34] O. Kuncar, A. Popescu, A consistent foundation for Isabelle/HOL, J. Autom. Reason. 62 (2019) 531–555. URL: https://doi.org/10.1007/s10817-018-9454-8. doi:10.1007/S10817- 018- 9454- 8. [35] O. Kuncar, A. Popescu, Safety and conservativity of definitions in HOL and Isabelle/HOL, Proc.
ACM Program. Lang. 2 (2018) 24:1–24:26. URL: https://doi.org/10.1145/3158112. doi:10.1145/ 3158112. [36] A. Gengelbach, T. Weber, Proof-theoretic conservative extension of HOL with ad-hoc overloading, in: V. K. I. Pun, V. Stolz, A. Simão (Eds.), Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings, volume 12545 of Lecture Notes in Computer Science, Springer, 2020, pp. 23–42. URL: https://doi.org/10.1007/ 978-3-030-64276-1_2. doi:10.1007/978- 3- 030- 64276- 1\_2.