Abstract The $$\lambda \varPi $$ λ Π -calculus modulo theory is an extension of simply typed $$\lambda $$ λ -calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the $$\lambda \varPi $$ λ Π -calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduce in the target theory a heterogeneous equality, and we build a translation that replaces each use of the conversion rule by the insertion of a transport. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms.

Abstract We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part of a broader research program aiming to define a logic with a proof language that forms a quantum programming language.

The lambda-Pi-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of U corresponding to each of these systems, and prove that, when a proof in U uses only symbols of a sub-theory, then it is a proof in that sub-theory.

We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.

Abstract User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom’s decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, confluence of a terminating set of left-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. The present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pairs. The rewrite relation used for analyzing confluence may rewrite arbitrarily many non-overlapping redexes in a single step. This relation gives rise to critical pairs that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. Practical examples of use of this technique are analyzed.

The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.

International audience

We define a notion of model for the lambda Pi-calculus modulo theory and prove a soundness theorem. We then define a notion of super-consistency and prove that proof reduction terminates in the lambda Pi-calculus modulo any super-consistent theory. We prove this way the termination of proof reduction in several theories including Simple type theory and the Calculus of constructions.

We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higher-order computation and linear algebra. This language extends the Lambda-calculus with the possibility to make arbitrary linear combinations of terms alpha.t + beta.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in the field of quantum computation, whose circuits we show can be easily encoded in the calculus. Finally, we prove the confluence of the entire calculus. Comment: The complementary note "On the critical pairs of a rewrite system for vector spaces" is provided in the source files. Short version : "Linear-algebraic Lambda-calculus : higher-order and confluence", Proceedings of RTA 08, Hagenberg, July 2008. LNCS 5117, 17, (2008). Long version : LMCS

Turing, in his immortal 1936 paper, observed that ‘[human] computing is normally done by writing… symbols on [two-dimensional] paper’, but noted that use of a second dimension ‘is always avoidable’ and that ‘the two-dimensional character of paper is no essential of computation’. We propose to promote two-dimensional models of computation and exploit the naturalness of two-dimensional representations of data. In particular, programs for a two-dimensional Turing machine can be recorded most naturally on its own two-dimensional input–output grid in such a transparent fashion that schoolchildren would have no difficulty comprehending their behaviour. This two-dimensional rendering allows, furthermore, for a most perspicacious rendering of Turing’s universal machine.

Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments. This allows for direct axiomatizations with binders, such as of the λ-binder of the lambda-calculus or the ∀-binder of first-order logic. It also allows us to finitely axiomatize arithmetic, and similarly to axiomatize “nominal” datatypes-with-binding. Just like first- and higher-order logic, equality reasoning is not necessary to α-rename. This gives PNL much of the expressive power of higher-order logic, but models and derivations of PNL are first-order in character, and the logic seems to strike a good balance between expressivity and simplicity.

Permissive-Nominal Logic (PNL) is an extension of first-order logic where term-formers can bind names in their arguments.

We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This method is complete in the sense that each normal proof-term of the formula is produced by some scheme generated by the grammar. As a corollary, we get a similar description of the set of normal proofs of positive formulae for a large class of theories including simple type theory and System F.

A high level model of the concept of operations of NASA's Small Aircraft Transportation System for Higher Volume Operations (SATS-HVO) is presented. The model is a non-deterministic, asynchronous transition system. It provides a robust notion of safety that relies on the logic of the concept rather than on physical constraints such as aircraft performances. Several safety properties were established on this model. The modeling and verification effort resulted in the identification of 9 issues, including one major flaw, in the original concept. Ten recommendations were made to the SATS-HVO concept development working group. All the recommendations were accepted and incorporated into the current concept of operations. The model was written in PVS. The verification is performed using an explicit state exploration algorithm written and proven correct in PVS.

Abstract We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.

We show in this note that cut elimination in deduction modulo subsumes cut elimination in deduction with the folding and unfolding rules.

Higher-order unification is equational unification for /spl beta//spl eta/-conversion, but it is not first-order equational unification, as substitution has to avoid capture. In this paper higher-order unification is reduced to first-order equational unification in a suitable theory: the /spl lambda//spl sigma/-calculus of explicit substitutions.

We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with η-conversion. Because these systems verify the proofs-as-objects paradigm, the proof synthesis method is a one-level process merging unification and resolution. Then we present a variant of this method, which is incomplete but much more efficient. Finally we show how to turn this algorithm into a unification algorithm.

The problem of determining whether a term is an instance of another in the simply typed lambda -calculus, i.e. of solving the equation a=b where a and b are simply typed lambda -terms and b is ground, is addressed. An algorithm that decides whether a matching problem in which all the variables are at most third order has a solution is given. The main idea is that if the problem a=b has a solution, then it also has a solution whose depth is bounded by some integer s depending only on the problem a=b, so a simple enumeration of the substitutions whose depth is bounded by s gives a decision algorithm. This result can also be used to bound the depth of the search tree in Huet's semi-decision algorithm and thus to turn it into an always-terminating algorithm. The problems that occur in trying to generalize the proof given to higher-order matching are discussed.>