Related papers: Lambda Calculus and Probabilistic Computation
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 prove the Stability Property for the call-by-value $\lambda$-calculus (CbV in the following). This result states necessary conditions under which the contexts of the CbV $\lambda$-calculus commute with intersections of approximants. This…
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…
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs,…
We introduce a linear infinitary $\lambda$-calculus, called $\ell\Lambda_{\infty}$, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted…
The denotational semantics of the untyped lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent…
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…
Programs with control are usually modeled using lambda calculus extended with control operators. Instead of modifying lambda calculus, we consider a different model of computation. We introduce continuation calculus, or CC, a deterministic…
The elegant theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are…
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…
The objective of this paper is to develop a functional programming language for quantum computers. We develop a lambda calculus for the classical control model, following the first author's work on quantum flow-charts. We define a…
We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution…
In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, $\lambda_\rho$, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide…
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive…
We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event lambda-calculus, a vehicle calculus in which both call-by-name…
The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential…
We consider the probabilistic applicative bisimilarity (PAB), a coinductive relation comparing the applicative behaviour of probabilistic untyped lambda terms according to a specific operational semantics. This notion has been studied with…
In compositional model-theoretic semantics, researchers assemble truth-conditions or other kinds of denotations using the lambda calculus. It was previously observed that the lambda terms and/or the denotations studied tend to follow the…
We study the desiderata on a model for statistical probabilistic programming languages. We argue that they can be met by a combination of traditional tools, namely open bisimulation and probabilistic simulation.
A $\lambda$-calculus is introduced in which all programs can be evaluated in probabilistic polynomial time and in which there is sufficient structure to represent sequential cryptographic constructions and adversaries for them, even when…