Related papers: Completeness of algebraic CPS simulations
We examine the relationship between the algebraic lambda-calculus, a fragment of the differential lambda-calculus and the linear-algebraic lambda-calculus, a candidate lambda-calculus for quantum computation. Both calculi are algebraic:…
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…
The algebraic $\lambda$-calculus is an extension of the ordinary $\lambda$-calculus with linear combinations of terms. We establish that two ordinary $\lambda$-terms are equivalent in the algebraic $\lambda$-calculus iff they are…
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…
We introduce two extensions of the $\lambda$-calculus with a probabilistic choice operator, $\Lambda_\oplus^{cbv}$ and $\Lambda_\oplus^{cbn}$, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that…
Probabilistic operational semantics for a nondeterministic extension of pure lambda calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics are both…
Applicative bisimulation is a coinductive technique to check program equivalence in higher-order functional languages. It is known to be sound, and sometimes complete, with respect to context equivalence. In this paper we show that…
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…
We study coupled logical bisimulation (CLB) to reason about contextual equivalence in the lambda-calculus. CLB originates in a work by Dal Lago, Sangiorgi and Alberti, as a tool to reason about a lambda-calculus with probabilistic…
This invited paper presents an overview of an ongoing research program aimed at extending the Curry-Howard-Lambek correspondence to quantum computation. We explore two key frameworks that provide both logical and computational foundations…
Algebraic lambda-calculi have been studied in various ways, but their semantics remain mostly untouched. In this paper we propose a semantic analysis of a general simply-typed lambda-calculus endowed with a structure of vector space. We…
We show that lambda calculus is a computation model which can step by step simulate any sequential deterministic algorithm for any computable function over integers or words or any datatype. More formally, given an algorithm above a family…
Recent developments in the categorical foundations of universal algebra have given fresh impetus to an understanding of the lambda calculus coming from categorical logic: an interpretation is a semi-closed algebraic theory. Scott's…
This paper introduces a formal metalanguage called the lambda-q calculus for the specification of quantum programming languages. This metalanguage is an extension of the lambda calculus, which provides a formal setting for the specification…
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…
Classical programming languages cannot model essential elements of complex systems such as true random number generation. This paper develops a formal programming language called the lambda-q calculus that addresses the fundamental…
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…
We define two extensions of the typed linear lambda-calculus that yield minimal Turing-complete systems. The extensions are based on unbounded recursion in one case, and bounded recursion with minimisation in the other. We show that both…
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 propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as…