相关论文: Quantum Lambda Calculi with Classical Control: Syn…

Scientists have demonstrated that quantum computing has presented novel approaches to address computational challenges, each varying in complexity. Adapting problem-solving strategies is crucial to harness the full potential of quantum…

In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus…

A non-deterministic call-by-need lambda-calculus \calc with case, constructors, letrec and a (non-deterministic) erratic choice, based on rewriting rules is investigated. A standard reduction is defined as a variant of left-most outermost…

The rapid progress of computer technology has been accompanied by a corresponding evolution of software development, from hardwired components and binary machine code to high level programming languages, which allowed to master the…

We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax where familiar programming constructs can have both quantum and…

Combinatory logic shows that bound variables can be eliminated without loss of expressiveness. It has applications both in the foundations of mathematics and in the implementation of functional programming languages. The original…

The lambda calculus with constructors is an extension of the lambda calculus with variadic constructors. It decomposes the pattern-matching a la ML into a case analysis on constants and a commutation rule between case and application…

We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without…

The investigation of quantum-classical correspondence may lead to gain a deeper understanding of the classical limit of quantum theory. We develop a quantum formalism on the basis of a linear-invariant theorem, which gives an exact…

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…

We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The…

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,…

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 introduce a Curry-Howard correspondence for a large class of intermediate logics characterized by intuitionistic proofs with non-nested applications of rules for classical disjunctive tautologies (1-depth intermediate proofs). The…

This paper demonstrates how to add a measurement operator to quantum lambda-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be…

We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent $\lambda$-calculi; each of them features a specific communication mechanism, including…

This paper establishes the normalisation of natural deduction or lambda calculus formulation of Intuitionistic Non Commutative Logic --- which involves both commutative and non commutative connectives. This calculus first introduced by de…

The claim that there is an inconsistency of quantum-classical dynamics [1] is investigated. We point out that a consistent formulation of quantum and classical dynamics which can be used to describe quantum measurement processes is already…

This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this…

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…