The -calculus forms one of the vertices in Barendregt's -cube and has been used as the core language for a number of logical frameworks. Following earlier extensions of natural deduction [14], Cousineau and Dowek [11] generalize the de nitional equality of this well studied calculus to an arbitrary congruence generated by rewrite rules, which allows for more faithful encodings of foreign logics. This paper motivates the resulting language, the -calculus modulo, as a universal proof language, capable of expressing proofs from many other systems without losing their computational properties. We further show how to very simply and e ciently check proofs from this language. We have implemented this scheme in a proof checker called Dedukti.
The success of formal methods since the pioneering e orts of the teams around LCF and Automath, both as tools of practical importance and as objects of intellectual curiosity, has spawned a bewildering variety of software systems to support them. While the eld has developed to maturity in academia and has registered some important successes in the industry, such as in aerospace, mass transit and smart cards to name a few, the full bene t of formal methods in an industrial setting remains largely untapped. We submit that a lack of standards and easy interoperability in the eld is one explanation to this state of a airs.
Indeed, the eld of formal methods has largely passed on the typical trend of other elds in computer science and engineering as they mature: the shift from systems to data. Standards have emerged for numbers, texts, images, sounds, videos, structured data, etc. These standards are not linked to a particular application, but all the applications comply to these standards, allowing the interoperability of various software, even on heterogeneous networks. When a community reaches a critical mass, standardization is unavoidable to allow exchange and collaborative improvements. As long as the use of proof systems was restricted to a small community, each system could develop its own independent language. But, this is not possible anymore: the success of proof systems and the widening of their audience put the interoperability problem to the fore.
Yet, importing and exporting lumps of proofs from system to system is a thorny issue, because di erent systems implement di erent formalisms: some are constructive, some are not, some are predicative, some are not, some are rst-order, some are not, etc. Thus, a standard must not only be able to de ne the proofs themselves, but also to specify the formalism in which they are expressed. To de ne such a standard, we propose the -calculus modulo, a simple but very powerful extension of a well-known and well understood proof language for minimal rst-order logic that embeds a congruence on types generated by a set of rewrite rules. 1.1
Avoiding the quadratic blowup in the number of adapters necessary between n di erent systems means introducing one common target for all these adapters. All foreign systems read and write a single proof format. One might hope to construct a formalism so powerful that other formalisms form a fragment of this super formalism, but this is infeasible in practice. For one, di erent formalisms require di erent but incompatible features, such as predicativity or impredicativity. Moreover, justifying the consistency of such a tower of Babel might not be quite so easy. Finally, the vast majority of proofs simply would not need the full power o ered by the formalism, only ever using a small fragment of it.
The alternative is to chose a simple formalism, say rst-order logic, and make other
formalisms the objects of discourse of this simple formalism. This is known as a deep embedding.
One will assert appropriate axioms to introduce these objects of discourse, such as axioms
characterizing the set of formulas, proof objects, validity judgments on proof objects, etc. This
is the approach used by Edinburgh Logical Framework [
Proofs, however, are not interesting merely for the validity of the judgment they establish. It can be desirable to reason about the proofs themselves. Realistic proofs of interesting facts typically contain detours in the reasoning. These detours often make the proof shorter, though they will usually be taken to be equivalent in some precise sense to a canonical derivation that does not contain any detours, or cuts. Eliminating cuts in a proof is a procedure, i.e. a computation.
When proofs are objects of discourse, it is convenient to be able to reason about them modulo elimination of any cuts. Many formalisms, such as the Calculus of Constructions or the original LF, include a powerful notion of de nitional equality that includes equality modulo cuts. Hence, identity of two proof objects can be established not by writing tedious reasoning steps, but rather by an appeal to this rather large de nitional equality, written ( ), which can be decided by applying the cut elimination procedure. The more powerful the de nitional equality, the more often derivations may appeal to it, hence the shorter they become.
Pure Type Systems (PTS), of which the Calculus of Constructions and LF are an instance, internalize de nitional equality using the following conversion rule: where s is some PTS dependent sort. Arguing that two objects are equal can be done in only one derivation step if they are de nitionally equal. The trouble here is that the notion of de nitional equality is xed once and for all, no matter the objects of discourse du jour. Hence, a deep embedding of foreign logics treats formulas, judgments and proofs of these logics as second class citizens | one can always de ne a judgment ( L) on proofs of a foreign logic L, but given two proofs P; Q in L, one can only justify P L Q using a derivation, not the native de nitional equality decision procedure.
In short, deep embeddings destroy the computational behaviour of proofs, because proof identity can no longer be justi ed computationally. Moreover, in general desirable properties such as canonicity of values and the existence of empty types are lost due to the presence of axioms. Many of these axioms uniquely characterize functions on the objects of discourse, for example as a set of equations. If only we could turn these equations into rewrite rules instead, we would be able to directly compute the results of applying these functions, rather than having to systematically prove using derivations that a function application is related to its result.
The -calculus modulo extends the -calculus, the core calculus of the original LF, with the ability to de ne one's own rewrite rules. The conversion rule above is modi ed to take de nitional equality to be an arbitrary congruence, generated by some set of user de ned rewrite rules R. In the -calculus modulo, we eschew equational axioms and instead turn them into rewrite rules. Intuitively, because the native de nitional equality is now extensible, when embedding a foreign logic within the -calculus modulo, we can tune the native de nitional equality to internalize the foreign de nitional equality. The computational behaviour of proofs is thus restored. The resulting embeddings are still deep embeddings, but we can introduce rewrite rules in a systematic way that essentially interpret a deep embedding into another shallow embeddings. 1.2
In the -calculus modulo, a theory is speci ed by a nite set of typed constants and a nite set of typed rewrite rules. This set of rules de nes the computational behavior of the set of constants. Encoding proofs of a logical system is achieved by writing a translation function from proofs of the original logical system to well typed terms of the -calculus modulo extended by the appropriate constants and rewrite rules. The same translations as the ones de ned for LF could be reused since LF is a strict subset of the -calculus modulo. However, in this case no bene t is drawn from the new computational facilities o ered by our framework and the computational properties of proof objects are lost.
We propose to use shallow embeddings as described above. Not only do proofs enjoy smaller
representations but consistency of theories can be proved with more generic techniques using,
for instance, super-consistency based approaches as described in [
To support this language, we propose a new proof-checker called Dedukti. A number of proof
checkers for similar logical frameworks have been proposed, such as Twelf [
This paper will rst present the -calculus modulo and motivate its use as a target language
for many other systems (Section 2). We will then describe informally the rationale behind a
purpose built proof-checker we have developped. A companion paper [
Context
is well-formed The -calculus modulo is a familiar formalism | it is a variation on the -calculus, which under the guise of many names (LF, P , etc), has been used with great success to specify other formalisms, from logics to programming languages. The -calculus is a simple proof language for minimal rst-order logic, whose syntax for pre-terms can be given succinctly as follows, provided we have an in nite set X of variable names:
M; N; A; B ::= x j x:A: M j
x:A: B j M N j Type j Kind
The notation A ! B stands for x:A: B when x does not appear in B. In the tradition of Pure
Type Systems (PTS) [
The type system for the -calculus, given in gure 1, does enforce a strati cation between sublanguages, that of terms, of types and of kinds: terms are typed by a type, types are typed by a kind and kinds are of type Kind.
Notice that in general types can be indexed by terms, giving a family of types, and that one can -abstract not only over terms but also over types. For these two reasons, -redexes can appear at the level of types and it is convenient to quotient them by -equivalence (written ( )) through the conversion rule. In gure 1, all the contexts are lists of pairs of a variable name and a type: ; ::=
j ; x:A congruence is generated by the -reduction rule alone, while in the generated by -reduction and the rewrite rules, as presented below. -calculus modulo it is Well-typed terms live within a context. One can segregate this context into a global shared context and a local context. We will write for this global context, which we call a signature and we assume to be well-formed. The assumptions of a signature are constants.
A system of rewrite rules is declared over constants of some signature . Each rewrite rule pertains to one constant of the signature. A typed rewrite rule is a rewrite rule paired with a typing context that assigns types to all the free variables appearing in the left hand side of the rule. Both sides of a rewrite rule must be typable with the same type A. De nition 1 (Rewrite rule). Let be a context. A rewrite rule in is a quadruple l ! ;A r composed of a context , and three -normal terms l; r; A, such that it is well-typed: the context ; is well-formed, and ; ` l : A and ; ` r : A are derivable judgments.
In order to use the rewrite rule, we must rewrite the instances of the left member by instances of the right member. Instances are done through typed substitutions.
De nition 2. Let ; is said to be of type Lemma 3. Let and of type . Then ; and
be contexts. A substitution binding the variables declared in if for any x:T 2 , we can derive ; ` x : T . be contexts, l ! ;T r be a rewrite rule in and be a substitution
` l : T and ; ` r : T and we say that l rewrites to r.
For a context and R a set of rewrite rules in , we let R be the smallest congruence generated by R. We write ( !) and ( ) (respectively) for the contextual closure and the smallest congruence generated by -reduction and R. 2.3
The claim of this paper is that the -calculus modulo can serve as a melting pot, capable of
expressing all manner of other type theories. This is in particular the case for all functional
PTS [
The typing rules of System F are identical to the rules of the -calculus that are presented in gure 1, except for the rules (prod) and (abs) that become: (F-prod) ` A : s `
; x : A ` B : Type x : A:B : Type (F-abs) ` A : s ; x`: Ax`:AB:M: T:ypex:A: B ; x : A ` M : B s 2 fType; Kindg System F is also strati ed into kinds (Type is the only kind), types and terms. For brevity and to lift any ambiguities, in the following we write ? (resp. 2) for the constant Type (resp. Kind) of System F. A typical example of term that is typable in System F is the polymorphic identity:
To encode System F in the -calculus modulo, we introduce four constants. U?; U2, also called universe constants re ect the types ? and 2 of System F in the -calculus modulo. To each universe is associated a decoding function " from System F types and function spaces to the native -calculus modulo types and function spaces.
U? : Type "2 : U2 ! Type "? : U? ! Type Now we introduce a constant that represents a deep embedding of the -types of System F as higher order abstract syntax into the -calculus modulo: Together with rewrite rules extending the decoding function to these System F types: _ h2;?;?i _ h?;?;?i : :
X:U2: ("2 X ! U?) ! U?
X:U?: ("? X ! U?) ! U? "? ( _ h2;?;?i X Y ) "? ( _ h?;?;?i X Y ) ! ! x:("2 X): "? (Y x) x:("? X): "? (Y x) Both rewrite rules have type Type (see De nition 1). They contain the free variables X and Y , so they are de ned (respectively) in the contexts:
X : U2; Y : ("2 X) X : U? ; Y : ("? X) ! U? ! U?
Cousineau and Dowek [
A : ("2 ?): ( _ h?;?;?i A ( x : ("? A): A)) i which, after simpli cation of "2 ? in U? and rewriting of the _ h2;?;?i constant gives the term: ` after -reduction and rewriting of ("2 ?), we get: and after another step of rewriting of the _ h?;?;?i: After -reduction and -conversion, we have: ` a judgment for which one can easily construct a derivation in the -calculus modulo.
Remark in particular how the use of higher order abstract syntax in the encoding of System F types a ords us substitution on those types for free. Also, polymorphism has been introduced in this term, through the constant "? that behave as a lifting from terms to types and from deep to shallow embeddings: this is clearly allowed by its nonempty computational content. Finally, conceivably one could along the same lines encode the -calculus into the -calculus modulo through the same mechanisms described above. This encoding would not be the identity (we would still have " and \dotted" constants appearing in types). 3 3.1
Dedukti's internal representation of terms is domain-free, as introduced in [
Contrary to the usual presentation of -calculus as a PTS, given in Section 2, the bidirectional type system we present in Figure 2 is syntax directed. As such, the choice of rule to apply at each step of the derivation is entirely determined by the shape of the term that is being typed. In particular, conversion only happens during a phase change between checking mode and synthesis mode. The moment at which this phase change is allowed to occur is guided by the \inputs" to the judgments. As such, the type system presented here is deterministic. One can therefore readily extract an algorithm from these typing rules: checking rules should be read as functions taking a context, a term and type as input and answering true or false; synthesis rules should be read as functions taking a context and term as input and producing a type as output. 3.2
One particularly thorny issue when checking dependently typed terms is the treatment of
renaming of variables to ensure that contexts remain well-formed and the implementation of
substitution. In keeping with the spirit of the de Bruijn criterion [
If in order to proceed to the body of abstractions it is necessary to unfold implementationlevel functions by feeding them parameters, we might as well feed more than just a parameter to these functions. We can indeed pass the type of the parameter along with it. In other words, we substitute a box | a pair of a term and its type | for bound variable as we move between bindings. We arrive in this way at a context-free type system, so-called because we no longer need to carry around a typing context in judgments, provided all free variables (parameters) in terms are always boxed. 3.3
The resulting type system, bidirectional and context-free, is given in Figure 2. A straightforward mapping of these rules into a purely functional program is discussed in Section 4. The syntax over which these rules are de ned is given below.
In its essence, a proof script consists of a sequence of non-recursive declarations of the form x : A. Later declarations have earlier declarations in scope. Proof scripts are type checked following the order of the sequence. Given a term M , checking that this term has some given type A will rst assume that A has already been type checked, just as the types of constants appearing in A may be assumed to already be checked when checking A. Therefore adding premises ensuring that contexts are well-formed to the leaf rules and mixing premises about types in the deduction rules for term typing as is done in the standard presentation of Section 2 does not accurately re ect how type checking works in practice. In the rules of Figure 2, the type A in a judgment ` M ( A is assumed to be a proper type or kind.
For the needs of type checking we can therefore use two distinct representations: one for the subject of a judgment (to the left of ) or (), underlined,
M ; N ; A; B ::= x j [y : A] j x: M j x:A: B j M N j Type and one for the classi er of a judgment (to the right of ) or (), overlined, M ; N ; A; B ::= x j y j x: M j x:A: B j M N j Type j Kind We reuse the same syntactic elements for both representations. The essential di erence between the two representations is that in the rst, parameters y are tagged with their type, whereas in the second parameters are bare. This is because it is not the classi ers that we are type checking, but only the subjects of typing judgments. The type of a parameter in a classi er is therefore not needed. We split the in nite set of variables into two disjoint in nite sets of (bound) variables x on the one hand and parameters y on the other. There is no way of binding parameters, because they stand in place of free variables.
In the rules of Figure 2, the judgment ` M ) A reads \the expression N synthesizes type A" and the judgment ` M ( A reads \the expression M checks against type A". Within judgments, we omit making the representation explicit through overlining and underlining, because which representation we mean is evident from the position in a judgment. In some rules we observe a crossover of subparts of the subject into the classi er and vice versa. In the (appb) rule, the argument part N crosses over to the right of the synthesis arrow. In the (absb) rule, the type A appears both in the subject part of a premise, but in the classi er part ` M ) A
Term M synthesizes type A (sortb) ` Type ) Kind (appb)
` M ) C ` M ( A
Term M checks against type A (absb) (prodb)
C !w
x:A: B ` M N ) fN=xgB ` x: M ( C `
x:A: B ( s ` N ) B ` N ( A
A
B C !w x:A: B
` f[y : A]=xgM ( fy=xgB ` A ( Type ` f[y : A]=xgB ( s
s 2 fType; Kindg (convb) (varb)
` [x : A] ) A ` N ( A This relation is left-total and right-unique, so that it determines a function from subject representations to classi er representations. Synthesis rules should be read top-down and checking rules bottom-up, so we don't need a coercion in the opposite direction.
In the (absb) and (prodb) rules, the new parameter y introduced in the premises must be chosen fresh. This condition can always be satis ed since terms are of nite size and the set of parameters is in nite.
Example 4. Consider the polymorphic identity as described in section 2. A type derivation for this term in the b-calculus modulo can be given as follows: x:("? y1): ("? y1) !w x:("? y1): ("? y1) A: ::: !w
A: ::: `
A: x: x (
` x: x ( A:U?: x:("? A): ("? A) x:("? y1): ("? y1) ` [y2 : "? y1] ) "? y1 ` [y2 : "? y1] ( "? y1 3.4
The algorithm presented here relies on nding the weak head normal form of types in order to proceed. This imposes that the set of rewrite rules used to generate the congruence ( ) veri es a certain number of properties for the algorithm to be deterministic and complete. Notice that reduction happens only on the classi er parts of a judgment. Reduction hence does not need to concern itself with dealing with boxes.
De nition 5 (Weak reduction). Given a set R of rewrite rules, we de ne weak reduction ( !w) as the contextual closure of the union of the usual -rule with R under the reduction context
C ::= [] j C M j M C j x:C: B Its re exive and transitive closure is written ( !w) and its re exive, transitive and symmetric closure is written ( w).
!w !w Type; !w Kind.
De nition 6 (Standardization). A relation on terms, provided it is con uent, is said to be standardizing if: 1. M x N1 : : : Nn implies M !w x N10 : : : N n0 and N1 N10 ; : : : ; Nn N n0; 2. M x: N implies M !w x: N 0 and N 0 N ; 3. M x:A: B implies M x:A0: B0 and A0 A and B0 B; 4. M Type implies M 5. M Kind implies M
If ( !) is con uent, standardizing and strongly normalizing, then it is su cient to compute
weak head normal forms [
Remark 7. The typing rules of this section are closer to an actual implementation of a type
checker, but a legitimate question to ask is how do we know that they are sound and complete
with respect to the typing rules of Figure 1. Coquand [
Rewrite rules can be classi ed according to the head constant to which they pertain. One can read the set of rewrite rules for one same head constant as clauses of a functional program, the left hand side of which contains a number of patterns.
However, contrary to an ordinary functional program, in the presence of dependent types matching one term might force the shape of another term. This will typically happen when a constructor forces one of the indexes of the type family in its result type. One simple example of this situation is the head function on vectors, de ned in the following signature:
Vector : n : Nat: Type
Z : Nat Nil : Vector Z
S : Nat ! Nat
Cons : n:Nat: Nat ! Vector n ! Vector (S n)
The type and the rewrite rule associated to the head function are:
head :
n:Nat: Vector n ! Nat
head fS ng (Cons n h tl)
! h
A non-linear pattern seems to be needed because n appears twice in its left hand side. We
cannot just generalize the rst pattern in this rewrite rule, because then the left hand side
would be ill-typed. A non-linear pattern would mean that we must check that the instances
for the two occurrences of n are convertible. Moreover, in general inductive type families might
be indexed by higher-order terms, meaning that we would need to implement higher-order
matching. However, what we actually want to express is that any instance to the rst pattern
of the rewrite rule above is uniquely determined by a matching instance of the second pattern.
Indeed, matching on the Cons constructor forces the dependent rst argument to head to be
S n. As such, the rst argument to head plays no operational role; it is merely there for the
sake of typing. Following Agda [
Note that the braces could equally have been placed around the n that is fed as argument to Cons. The only important property to verify is that one and only one occurrence of n must not have braces. This occurrence will be the one that binds n. 4
We have by now developed an abstract characterization of a proof checking algorithm. However, we have not so far been explicit about how to implement substitution on terms, nor have we discussed how to decide de nitional equality algorithmically. Ideally, whatever implementation we choose, it should be both simple and e cient. Indeed, encodings in the style of Section 2.3 introduce many more redexes in types than were present in the original input. Moreover, computing the weak head normal form of some types may require an arbitrarily large number of reductions, even before any encoding overhead, such as can be the case in proofs by re ection.
Normalization by evaluation (NbE) is one particularly easy to implement normalization
scheme that alternates phases of weak reduction (i.e. evaluation) and rei cation phases (or
readback phases [
1A term may contain parameters but those cannot be captured: there are no binding forms for parameters in the syntax of terms. jjxjj = x jjyjj = VarC y jj x: M jj = LamC ( x ! jjM jj) jj x:A: Bjj = PiC jjAjj ( x ! jjBjj) jjM N jj = app jjM jj jjN jj jjTypejj = TypeC jjKindjj = KindC (a)
jxj = x j[y : A]j = BoxT y j x: M j = LamT ( x ! jM j) j x:A: Bj = PiT jAj ( x ! jBj) jM N j = AppT jM j jN j jTypej = TypeT (b)
For simplicity, we use an untyped variant of NbE, in the style of [
The actual identity of a bound variable is usually quite irrelevant2. What is relevant is to be able to conveniently substitute another term for all free occurrences of a variable under its binder. Paramaters are dual, in that we never need to substitute for a parameter, nor do they have scope since they cannot be bound, but their identity is crucial. During type-checking, we must be able to ask whether this parameter is the same as this other parameter.
We therefore map (bound) variables to variables of the target language, allowing us to piggy back substitution and scope management onto that of the target language. We get substitution essentially for free. Parameters, on the other hand, are a ground piece of data: a name. Here, for simplicity, we use integers for names.
In a similar spirit, we wish to reuse the target language's computational facilities to reduce terms to normal forms. Therefore applications are mapped to target language applications. However, our embedding of terms in the target language is not quite shallow, in that functions and so on are not represented directly as functions of the target language but rather as values of type Code. This embedding into a monomorphic datatype is essentially an untyped embedding, thus avoiding the impedence mismatch between the type system of the -calculus modulo and that of the target language, in our case Haskell. Therefore we must introduce app, a wrapper function around the native application operation, which essentially decapsulates functions embedded in values of type Code:
app :: Code ! Code ! Code 2Indeed this is why formal developments in the presence of binding internalize Barendregt's variable convention in some form. app (LamC f ) t = f t app t1 t2 = AppC t1 t2 If the rst argument of app is a function, then we can proceed with the application. If not, we are stuck, and the result is a neutral term.
Deciding the equality between two terms can now be done near structurally: conv :: Int ! Code ! Code ! Bool conv n (VarC x ) (VarC x 0) = x x 0 conv n (LamC t ) (LamC t 0) = conv (n + 1) (t (VarC n)) (t 0 (VarC n)) conv n (PiC ty1 ty2) (PiC ty3 ty4) = conv n ty1 ty3 ^
conv (n + 1) (ty2 (VarC n)) (ty4 (VarC n)) conv n (AppC t1 t2) (AppC t3 t4) = conv n t1 t3 ^ conv n t2 t4 conv n TypeC TypeC = True conv n KindC KindC = True conv n = False Descending under binding structures gives the weak head normal form of their body, which is computed automatically according to the semantics of the target language. The rst argument serves as a supply of fresh parameter names; these need only be locally unique so a local supply is su cient.
We now have a succinct and yet e cient way of deciding equality of two terms that we know to be well-typed. The translation of Figure 3 for classi ers isn't appropriate, however, for subjects of type checking, because contrary to classi ers, subjects are not a priori welltyped. Therefore, we cannot assume that any kind of normal form exists for subjects, lest we compromise the decidability of type checking. We therefore introduce an alternative translation for subjects, where terms are not identi ed modulo any reduction. This translation is given in part (b) of Figure 3. Note that it is a completely standard mapping of terms to higher order abstract syntax, into values of following datatype: data Term = BoxT Code Code j AppT Term Term j LamT (Term ! Term) j PiT Term (Term ! Term) j TypeT One particularly nice feature of this translation is that it di ers from that for classi ers in one single place: the interpretation of applications.
In Dedukti, to control the amount of code that we generate, and to avoid writing wasteful coercions between values of type Term and values of type Code, which we would have to invoke at every application node in the term that we are checking, we generate a single Haskell source for a single proof script, containing both the subject translation and classi er translation for every subterm of the proof script. That is, Term and Code representations are tied together for every subterm, through a system of pairing (or gluing). This way no coercion is necessary, but if we performed this gluing naively, it would obviously provoke and explosion in the size of the generated code. The size would grow exponentially with the tree depth of terms, because we would be duplicating subtrees at every level.
For this reason, in the actual implementation, we rst transform terms into a linear form,
namely A-normal form. In this form, all subterms are named, so that it becomes possible
to share substructures of translations at every level, hence avoiding any kind of exponential
blowup. The rationale for this translation is similar to that of let-insertion to avoid blowups
during partial evaluation [
Both of these standard code transformations can be performed selectively, only for subterms where both the subject and classi er representations are needed (both forms are need only when checking applications M N , and then only when the type synthesized for M is of the form x:A: B where x does occur in B). If we commit to a particular rewrite strategy, and for convenience we commit to a particular rewrite strategy that matches the evaluation order of the target language, then we can extend the scheme given previously to gracefully handle custom rewrite rules. The idea is to read the rewrite rules for one same head constant as the clauses of a functional program. This is the idea behind the translation of rewrite rules as functional programs over values of type Code given in Figure 4. The resulting functional program implements the rewrite rules in exactly the same way that the app function implements -reduction; if for a given subterm none of the rewrite rules apply, then the result is a neutral term. 5
We have presented in this paper a simple and extensible calculus that works well as a common format for a large number of other proof systems. The essential di erence with previous proposals is that through an extensible de nitional equality, the -calculus modulo can act as a logical framework that respects the computational properties of proofs. We showed how this calculus can be implemented very succinctly by leveraging existing evaluation technology.
Our approach is rmly grounded in type theory; computation only happens as a result of
checking for convertibility between two types, just as in other type theories. Other recent e orts
for a common proof format, such as the proposal of Miller [
We have an implementation of a proof checker, Dedukti, which expects the system of rewrite rules provided by the user to be reasonably well behaved. This proof checker is therefore only one small piece of the larger puzzle: con dence in the results of this tool are contingent upon trusting that the provided rewrite rules do not compromise logical consistency, or that these rewrite rules indeed form a con uent and terminating system. Dedukti only checks types, it does not check the rewrite rules. Future work will focus providing these other pieces to support our methodology: tools to (semi-)automatically verify properties about rewrite rules, for example.
For given translations, a system of rewrite rules or a schema of rewrite rules need only be proven to behave properly once, rather than every time for every results of these translations. However, we could also envisage making the -calculus modulo the core of a full edged proof environment for end users, in which users can de ne their own domain speci c rewrite rules, in which case automated certi cation of properties about the resulting system of rewrite rules becomes essential.
We are currently working on adapting size-based termination techniques [
Finally, we currently type check by rst translating proofs and formulas into a functional program in Haskell, which we compile to native code using the GHC compiler. However, the compilation process is slow. Its cost is only amortized given proofs with signi cant computational content and even then, we would rather not have the compiler waste time optimizing parts of the proof that are computationally completely irrelevant. Other systems such as Coq and Isabelle ask the user to decide exactly when to use an optimizing compiler and when to compute using a much more lightweight interpreter. The advantage of our approach is its simplicity, both for the user and for the implementation. We would like to keep this model, but to make it scale, we are investigating translating terms to a language that supports \just in time" compilation, whereby hotspots that are worth compiling to native code are identi ed at runtime and automatically, still without any intervention from the user.
A stable release of Dedukti is available at https://www.rocq.inria.fr/deducteam/ Dedukti/index.html, however some of the improvements discussed here (in particular, the dot patterns of section 3.5) have been integrated only in the development version of Dedukti, that can be found on Github: https://github.com/mpu/dedukti.