相关论文: From X to Pi; Representing the Classical Sequent C…

We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike $\lambda$-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names…

Types are an important part of any modern programming language, but we often forget that the concept of type we understand nowadays is not the same it was perceived in the sixties. Moreover, we conflate the concept of "type" in programming…

Induction is typically formalized as a rule or axiom extension of the LK-calculus. While this extension of the sequent calculus is simple and elegant, proof transformation and analysis can be quite difficult. Theories with an induction…

Computation can be considered by taking into account two dimensions: extensional versus intensional, and sequential versus concurrent. Traditionally sequential extensional computation can be captured by the lambda-calculus. However, recent…

We study polymorphic type assignment systems for untyped lambda-calculi with effects, based on Moggi's monadic approach. Moving from the abstract definition of monads, we introduce a version of the call-by-value computational…

Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a…

We express quantum computations (with measurements) using the arrow calculus extended with monadic constructions. This framework expresses quantum programming using well-understood and familiar classical patterns for programming in the…

This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably,…

The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization in type theory. We present a new set of type classes for mathematics and take full advantage…

The lambda Pi calculus can be extended with rewrite rules to embed any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda…

In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies…

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…

We consider two characterisations of the may and must testing preorders for a probabilistic extension of the finite pi-calculus: one based on notions of probabilistic weak simulations, and the other on a probabilistic extension of a…

We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagner's counting hierarchy,…

Starting from the observation that distinct notions of copying have arisen in different categorical fields (logic and computation, contrasted with quantum mechanics) this paper addresses the question of when, or whether, they may coincide.…

We present a quantum compilation algorithm that maps Clifford encoders, encoding maps for stabilizer quantum codes, to a unique graphical representation in the ZX calculus. Specifically, we develop a canonical form in the ZX calculus and…

We construct a functor from the Hecke category to a groupoid built from the underlying Coxeter group. This fixes a gap in an earlier work of the authors. This functor provides an abstract realization of the localization of the Hecke…

The classes of depth-bounded and name-bounded processes are fragments of the pi-calculus for which some of the decision problems that are undecidable for the full calculus become decidable. P is depth-bounded at level k if every reduction…

Message passing is a key ingredient of concurrent programming. The purpose of this paper is to describe the equivalence between the proof theory, the categorical semantics, and term calculus of message passing. In order to achieve this we…

The S-pi-calculus is a synchronous pi-calculus which is based on the SL model. The latter is a relaxation of the Esterel model where the reaction to the absence of a signal within an instant can only happen at the next instant. In the…