Related papers: Isomorphisms considered as equalities: Projecting …
We provide a proof of strong normalisation for lambda+, a recently introduced, explicitly typed, non-deterministic lambda-calculus where isomorphic propositions are identified. Such a proof is a non-trivial adaptation of the reducibility…
System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an extension of System I to polymorphic types, adding the…
We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms…
The linear-algebraic lambda-calculus and the algebraic lambda-calculus are untyped lambda-calculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while…
We describe a type system for the linear-algebraic $\lambda$-calculus. The type system accounts for the linear-algebraic aspects of this extension of $\lambda$-calculus: it is able to statically describe the linear combinations of terms…
Quantum lambda calculus has been studied mainly as an idealized programming language -- the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum…
We introduce a simple extension of the $\lambda$-calculus with pairs---called the distributive $\lambda$-calculus---obtained by adding a computational interpretation of the valid distributivity isomorphism $A \Rightarrow (B\wedge C)\ \…
The $\lambda$-calculus is a handy formalism to specify the evaluation of higher-order programs. It is not very handy, however, when one interprets the specification as an execution mechanism, because terms can grow exponentially with the…
The $\lambda$$\Pi$-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…
To support the understanding of declarative probabilistic programming languages, we introduce a lambda-calculus with a fair binary probabilistic choice that chooses between its arguments with equal probability. The reduction strategy of the…
In this paper, we present an extension of $\lambda\mu$-calculus called $\lambda\mu^{++}$-calculus which has the following properties: subject reduction, strong normalization, unicity of the representation of data and thus confluence only on…
In this paper, we present a general realizability semantics for the simply typed $\lambda\mu$-calculus. Then, based on this semantics, we derive both weak and strong normalization results for two versions of the $\lambda\mu$-calculus…
With a view towards models of quantum computation and/or the interpretation of linear logic, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an…
The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine, and continues to be of…
Probabilistic applicative bisimulation is a recently introduced coinductive methodology for program equivalence in a probabilistic, higher-order, setting. In this paper, the technique is applied to a typed, call-by-value, lambda-calculus.…
Correctness of program transformations in extended lambda calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach to proving correctness is the…
This paper introduces a new term rewriting system that is similar to the embedded read-back mechanism for interaction nets presented in our previous work, but is easier to follow than in the original setting and thus to analyze its…
We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded…
On the topic of probabilistic rewriting, there are several works studying both termination and confluence of different systems. While working with a lambda calculus modelling quantum computation, we found a system with probabilistic…
We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In…