A formalised first-order confluence proof for the λ-calculus using one-sorted variable names

We present the titular proof development that has been verified in Isabelle/HOL. As a first, the proof is conducted exclusively by the primitive proof principles of the standard syntax and of the considered reduction relations: the naive way, so to speak. Curiously, the Barendregt Variable Convention takes on a central technical role in the proof. We also show: (i) that our presentation of the λ-calculus coincides with Curry’s and Hindley’s when terms are considered equal up to α-equivalence and (ii) that the confluence properties of all considered systems are equivalent.     

Bounded Model Generation for Isabelle/HOL

A translation from higher-order logic (on top of the simply typed λ-calculus) to propositional logic is presented, such that the resulting propositional formula is satisfiable iff the HOL formula has a model of a given finite size. A standard SAT solver can then be used to search for a satisfying assignment, and such an assignment can be transformed back into a model for the HOL formula. The algorithm has been implemented in the interactive theorem prover Isabelle/HOL, where it is used to automatically generate countermodels for non-theorems.     

Term Collections in λ and ρ-calculi

The ρ-calculus generalises term rewriting and the λ-calculus by defining abstractions on arbitrary patterns and by using a pattern-matching algorithm which is a parameter of the calculus. In particular, equational theories that do not have unique principal solutions may be used. In the latter case, all the principal solutions of a matching problem are stored in a “structure” that can also be seen as a collection of terms.Motivated by the fact that there are various approaches to the definition of structures in the ρ-calculus, we study in this paper a version of the λ-calculus with term collections.The contributions of this work include a new syntax and operational semantics for a λ-calculus with term collections, which is related to the λ-calculi with strict parallel functions studied by Boudol and Dezani et al. and a proof of the confluence of the β-reduction relation defined for the calculus (which is a suitable extension of the standard rule of β-reduction in the λ-calculus).     

Strong normalisation in the π-calculus

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.     

Soundness and Completeness Proofs by Coinductive Methods

We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an abstract property of possibly infinite derivation trees. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems for various flavors of first-order logic. Soundness becomes interesting as soon as one allows infinite proofs of first-order formulas. This forms the subject of several cyclic proof systems for first-order logic augmented with inductive predicate definitions studied in the literature. All the discussed results are formalized using Isabelle/HOL’s recently introduced support for codatatypes and corecursion. The development illustrates some unique features of Isabelle/HOL’s new coinductive specification language such as nesting through non-free types and mixed recursion–corecursion.     

Database Query Languages Embedded in the Typed Lambda Calculus

We investigate the expressive power of the typedλ-calculus when expressing computations over finite structures, i.e., databases. We show that the simply typedλ-calculus can express various database query languages such as the relational algebra, fixpoint logic, and the complex object algebra. In our embeddings, inputs and outputs areλ-terms encoding databases, and a program expressing a query is aλ-term which types when applied to an input and reduces to an output. Our embeddings have the additional property that PTIME computable queries are expressible by programs that, when applied to an input, reduce to an output in a PTIME sequence of reduction steps. Under our database input-output conventions, all elementary queries are expressible in the typedλ-calculus and the PTIME queries are expressible in the order-5 (order-4) fragment of the typedλ-calculus (with equality).     

On the representation of McCarthy's in the -calculus

We study the encoding of , the call-by-name λ-calculus enriched with McCarthy's amb operator, into the π-calculus. Semantically, amb is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the λ-calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong divergence), the encoding is possible, and for this case we derive results and coinductive proof methods to reason about that are similar to those for the encoding of pure λ-calculi. We then use these methods to derive the most important laws concerning amb. We take bisimilarity as behavioural equivalence on the π-calculus, which sheds some light on the relationship between fairness and bisimilarity.     

A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations

A formalized theory of alpha-conversion for the π-calculus in Isabelle/HOL is presented. Following a recent proposal by Gabbay and Pitts, substitutions are modelled in terms of permutations, and alpha-equivalence is defined over all but finitely many names. In contrast to the work by Gabbay and Pitts, however, standard universal and existential quantification are used instead of introducing a new binder.Further, a classification of the various approaches to formalizing languages with binders is presented. Strengths and weaknesses are pointed out, and suggestions for possible applications are made.     

Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus

We present a call-by-need λ-calculus λ_ND with an erratic non-deterministic operator pick and a non-recursive let. A definition of a bisimulation is given, which has to be based on a further calculus named λ_≈, since the naïve bisimulation definition is useless. The main result is that bisimulation in λ_≈ is a congruence and coincides with the contextual equivalence. The proof is a non-trivial extension of Howe's method. This might be a step towards defining useful bisimulation relations and proving them to be congruences in calculi that extend the λ_ND-calculus.     

Coinductive Verification of Program Optimizations Using Similarity Relations

Formal verification methods have gained increased importance due to their ability to guarantee system correctness and improve reliability. Nevertheless, the question how proofs are to be formalized in theorem provers is far from being trivial, yet very important as one needs to spend much more time on verification if the formalization was not cleverly chosen. In this paper, we develop and compare two different possibilities to express coinductive proofs in the theorem prover Isabelle/HOL. Coinduction is a proof method that allows for the verification of properties of also non-terminating state-transition systems. Since coinduction is not as widely used as other proof techniques as e.g. induction, there are much fewer “recipes” available how to formalize corresponding proofs and there are also fewer proof strategies implemented in theorem provers for coinduction. In this paper, we investigate formalizations for coinductive proofs of properties on state transition sequences. In particular, we compare two different possibilities for their formalization and show their equivalence. The first of these two formalizations captures the mathematical intuition, while the second can be used more easily in a theorem prover. We have formally verified the equivalence of these criteria in Isabelle/HOL, thus establishing a coalgebraic verification framework. To demonstrate that our verification framework is suitable for the verification of compiler optimizations, we have introduced three different, rather simple transformations that capture typical problems in the verification of optimizing compilers, even for non-terminating source programs.     

Descendants and Origins in Term Rewriting

In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first-order term rewriting and λ-calculus, their finitary as well as their infinitary variants. A recurrent theme is the parallel moves lemma. Next to the classical notion of descendant, we introduce an extended version, known as origin tracking. Origin tracking has many applications. Here it is employed to give new proofs of three classical theorems: the genericity lemma in λ-calculus, the theorem of Huet and Lévy on needed reductions in first-order term rewriting, and Berry's sequentiality theorem in (infinitary) λ-calculus.     

Confluence of Curried Term-Rewriting Systems

Term rewriting systems operate on first-order terms. Presenting such terms in curried form is usually regarded as a trivial change of notation. However, in the absence of a type-discipline, or in the presence of a more powerful type-discipline than simply typed λ-calculus, the change is not as trivial as one might first think.It is shown that currying preserves confluence of arbitrary term rewriting systems. The structure of the proof is similar to Toyama's proof that confluence is a modular property of TRS.     

Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle’s built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver.     

Developing (Meta)Theory of λ-calculus in the Theory of Contexts

We present a case study on the formal development of a non trivial (meta)theory in the Theory of Contexts using the Coq proof assistant. The methodology underlying the Theory of Contexts for reasoning on systems presented in HOAS is based on an axiomatic syntactic standpoint. We feel that one of the main advantages of this approach, is that it requires a very low logical overhead.The object system we focus on is the lazy, call-by-name λ-calculus (λ_cbn), both untyped and simply typed. We will see that the formal, fully detailed development of the theory of (λ_cbn) in the Theory of Contexts introduces a small, sustainable overhead with respect to the proofs “on the paper”. Moreover, this will allow for comparison with similar case studies developed in other approaches to the metatheoretical reasoning in higher-order abstract syntax.     

Semi-intelligible Isar Proofs from Machine-Generated Proofs

Sledgehammer is a component of the Isabelle/HOL proof assistant that integrates external automatic theorem provers (ATPs) to discharge interactive proof obligations. As a safeguard against bugs, the proofs found by the external provers are reconstructed in Isabelle. Reconstructing complex arguments involves translating them to Isabelle’s Isar format, supplying suitable justifications for each step. Sledgehammer transforms the proofs by contradiction into direct proofs; it iteratively tests and compresses the output, resulting in simpler and faster proofs; and it supports a wide range of ATPs, including E, LEO-II, Satallax, SPASS, Vampire, veriT, Waldmeister, and Z3.     

A Mechanized Proof of the Basic Perturbation Lemma

We present a complete mechanized proof of the result in homological algebra known as basic perturbation lemma. The proof has been carried out in the proof assistant Isabelle, more concretely, in the implementation of higher-order logic (HOL) available in the system. We report on the difficulties found when dealing with abstract algebra in HOL, and also on the ongoing stages of our project to give a certified version of some of the algorithms present in the Kenzo symbolic computation system. J. Aransay was partially supported by Ministerio de Educación y Ciencia, MTM2006/06513, and by Gobierno de La Rioja ANGI2005/19 and J. Rubio was partially supported by Ministerio de Educación y Ciencia, MTM2006/06513, and by Gobierno de La Rioja ANGI2005/19.     

Extending Sledgehammer with SMT Solvers

Sledgehammer is a component of Isabelle/HOL that employs resolution-based first-order automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically selects relevant facts and, if an ATP is successful, produces a snippet that replays the proof in Isabelle. We extended Sledgehammer to invoke satisfiability modulo theories (SMT) solvers as well, exploiting its relevance filter and parallel architecture. The ATPs and SMT solvers nicely complement each other, and Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs’ reach.     

Proving pointer programs in higher-order logic

Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. The programming language is embedded in higher-order logic. Its Hoare logic is derived. The whole development is purely definitional and thus sound. Apart from some smaller examples, the viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr–Waite graph marking algorithm and present part of its readable proof in Isabelle/HOL.     

Semantics,calculi, and analysis for object-oriented specifications

We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/hol and the language is oriented towards ocl formulae in the context of uml class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.     

Infinite intersection types

A type theory with infinitary intersection and union types for an extension of the λ-calculus is introduced. Types are viewed as upper closed subsets of a Scott domain and intersection and union type constructors are interpreted as the set-theoretic intersection and union, respectively, even when they are not finite. The assignment of types to λ-terms extends naturally the basic type assignment system. We prove soundness and completeness using a generalization of Abramsky’s finitary logic of domains. Finally, we apply the framework to applicative transition systems, obtaining a sound a complete infinitary intersection type assignment system for the lazy λ-calculus.