Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle.

In the theory of sequential programming languages, Berry's stability property is an important step claiming that values have unique origins in their calculations. It has been shown that Bohm trees are stable in the λ-calculus, meaning that there is a unique minimum prefix of any lambda term which computes its Bohm tree. Moreover this property is also true for finite prefixes of Bohm trees. The proof relies on Curry's standardization theorem as initially pointed out by Plotkin in his famous articleLCF considered as a programming language. In this paper we will show that the stability property also holds for redexes. Namely for any redex family, there is a unique minimum calculation and a unique redex which computes this family. This property was already known in the study of optimal reductions, but we stress here on stability and want to show that stability is inside the basic objects of calculations. The proof will be based on nice commutations between residuals and creations of new redexes. Our tool for proving this property will be the labelled lambda calculus used in the study of optimal reductions.

A new “inductive” approach to standardization for the λ-calculus has been recently introduced by Xi, allowing him to establish a double-exponential upper bound |M|2|σ|for the length of the standard reduction relative to an arbitrary reduction σ originated in M. In this paper we refine Xi's analysis, obtaining much better bounds, especially for computations producing small normal forms. For instance, for terms reducing to a boolean, we are able to prove that the length of the standard reduction is at most a mere factorial of the length of the shortest reduction sequence. The methodological innovation of our approach is that instead of counting the cost for producing something, as is customary, we count the cost of consuming things. The key observation is that the part of a λ-term that is needed to produce the normal form (or an arbitrary rigid prefix) may rapidly augment along a computation, but can only decrease very slowly (actually, linearly).

We address the problem of dependency analysis and caching in the context of the λ-calculus. The dependencies of a λ-term are (roughly) the parts of the λ-term that contribute to the result of evaluating it. We introduce a mechanism for keeping track of dependencies, and discuss how to use these dependencies in caching.

Categorical combinators [Curien 1986/1993; Hardin 1989; Yokouchi 1989] and more recently λσ-calculus [Abadi 1991; Hardin and Le´vy 1989], have been introduced to provide an explicit treatment of substitutions in the λ-calculus. We reintroduce here the ingredients of these calculi in a self-contained and stepwise way, with a special emphasis on confluence properties. The main new results of the paper with respect to Curien [1986/1993], Hardin [1989], Abadi [1991], and Hardin and Le´vy [1989] are the following: (1) We present a confluent weak calculus of substitutions, where no variable clashes can be feared; (2) We solve a conjecture raised in Abadi [1991]: λσ-calculus is not confluent (it is confluent on ground terms only). This unfortunate result is “repaired” by presenting a confluent version of λσ-calculus, named the λ Env -caldulus in Hardin and Le´vy [1989], called here the confluent λσ-calculus.

J.-Y. Girard's original definition of proof nets for linear logic involves boxes. The box is the unit for erasing and duplicating fragments of proof nets. It imposes synchronization, limits sharing, and impedes a completely local view of computation. The authors describe an implementation of proof nets without boxes. Proof nets are translated into graphs of the sort used in optimal lambda -calculus implementations; computation is performed by simple graph rewriting. This graph implementation helps in understanding optimal reductions in the lambda -calculus and in the various programming languages inspired by linear logic.>

An axiomatic version of the standardization theorem that shows the necessary basic properties between nesting of redexes and residuals is presented. This axiomatic approach provides a better understanding of standardization, and makes it applicable in other settings, such as directed acyclic graphs (dags) or interaction networks. conflicts between redexes are also treated. The axioms include stability in the sense given by G. Berry (Ph.D. thesis, Univ. of Paris, 1979), proving it to be an intrinsic notion of deterministic calculi.>

Lamping discovered an optimal graph-reduction implementation of the λ-calculus. Simultaneously, Girard invented the geometry of interaction, a mathematical foundation for operational semantics. In this paper, we connect and explain the geometry of interaction and Lamping's graphs. The geometry of interaction provides a suitable semantic basis for explaining and improving Lamping's system. On the other hand, graphs similar to Lamping's provide a concrete representation of the geometry of interaction. Together, they offer a new understanding of computation, as well as ideas for efficient and correct implementations.

Abstract The λσ-calculus is a refinement of the λ-calculus where substitutions are manipulated explicitly. The λσ-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical λ-calculus and concrete implementations.

The λσ-calculus is a refinement of the λ-calculus where substitutions are manipulated explicitly. The λσ-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical λ-calculus and concrete implementations.

Vufllemm's results on opumal computations of recurswe programs are generalized New syntactic results are obtained by considering spaces of denvauons instead of terms The results apply to classes of mterpretauons more general than the sequential interpretations of Vmllemm

Procedure call mechanisms have mainly been studied in the framework of recursive programs without assignments, for the simplicity of their operational and denotational semantics (See Scott [16], Nivat [14], Vuillemin [17]).