Related papers: Calculi for Intuitionistic Normal Modal Logic
Existing Curry-Howard interpretations of call-by-value evaluation for the $\lambda$-calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additional logical concepts such as classical logic or linear…
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…
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…
This paper extends the dual calculus with inductive types and coinductive types. The paper first introduces a non-deterministic dual calculus with inductive and coinductive types. Besides the same duality of the original dual calculus, it…
In each variant of the lambda-calculus, factorization and normalization are two key-properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants…
This paper introduces a natural deduction calculus for intuitionistic logic of belief $\mathsf{IEL}^{-}$ which is easily turned into a modal $\lambda$-calculus giving a computational semantics for deductions in $\mathsf{IEL}^{-}$. By using…
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…
Under the extension of Curry-Howard's correspondence to classical logic, Gentzen's NK and LK systems can be seen as syntax-directed systems of simple types respectively for Parigot's Lambda Mu Calculus and Curien-Herbelin's Lambda Bar Mu Mu…
We offer a simple graphical representation for proofs of intuitionistic logic, which is inspired by proof nets and interaction nets (two formalisms originating in linear logic). This graphical calculus of proofs inherits good features from…
We provide characterization of the strong termination property of the CCV (complete call-by-value) lambda-mu calculus introduced in the first part of this series of the paper. The calculus is complete with respect to the standard…
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…
This reports introduces a novel sound and complete semantics for first order intuitionistic logic, in the framework of category theory and by the computational interpretation of the logic based on the so-called Curry-Howard isomorphism.…
This is a survey of {\lambda}-calculi that, through the Curry-Howard isomorphism, correspond to constructive modal logics. We cover the prehistory of the subject and then concentrate on the developments that took place in the 1990s and…
We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and…
We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the pi-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed…
Under the Curry--Howard isomorphism, the syntactic structure of programs can be modeled using birelational Kripke structures equipped with intuitionistic and modal relations. Intuitionistic relations capture scoping through persistence,…
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…
We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-name executions of programs often have different, but related,…
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…
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…