We present a new Curry–Howard correspondence for classical first-order natural deduction. We add to the lambda calculus an operator which represents, from the viewpoint of programming, a mechanism ...for raising and catching multiple exceptions, and from the viewpoint of logic, the excluded middle over arbitrary prenex formulas. The machinery will allow to extend the idea of learning – originally developed in Arithmetic – to pure logic. We prove that our typed calculus is strongly normalizing and show that proof terms for simply existential statements reduce to a list of individual terms forming an Herbrand disjunction. A by-product of our approach is a natural-deduction proof and a computational interpretation of Herbrand's Theorem.
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of ...message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O’Hearn and Pym’s Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new π-calculus with sessions, called πBI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of πBI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine λ-calculus; and a non-interference result for access of resources.
Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder ...view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient to proper propositions. The Curry–Howard correspondence is typically viewed as a formal counterpart of this conception. I will argue against this position and show that even though the Curry–Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted.
Curry and Howard Meet Borel Antonelli, Melissa; Dal Lago, Ugo; Pistone, Paolo
Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science,
08/2022
Conference Proceeding
Open access
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 λ-calculus, a vehicle ...calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but reveal the underlying probability. We finally show how to obtain a system precisely capturing the probabilistic behavior of λ-terms, by endowing the type system with an intersection operator.
This paper extends previous work on the modal logic
CK
as a reference system, both proof-theoretically and model-theoretically, for a correspondence theory of constructive modal logics. First, the ...fundamental nature of
CK
is discussed and compared with the intuitionistic modal logic
IK
which is traditionally taken to be the base line. Then, it is shown, that
CK
admits of a cut-free Gentzen sequent calculus
G
-
CK
which has (i) a local interpretation in constructive Kripke models and (ii) does not require explicit world labels. Finally, the paper demonstrates how non-classical modal logics such as
IK
,
C
S
4
,
CL
, or Masiniʼs deontic system of 2-sequents arise as theories of
CK
, presented both as special rules and as frame classes.
Abstract
Atomic polymorphism $\mathbf{F_{at}}$ is a restriction of Girard and Reynold’s system $\mathbf{F} $(or $\lambda 2$) which was first introduced in Ferreira
2 in the context of a ...philosophical commentary on predicativism. $\lambda 2$ is a well-known and powerful formal tool for studying polymorphic functional programming languages and formal methods in program specification and development, but its computational power far exceeds the recursive level of interest in applications. Hence, the interest of studying subsystems of $\lambda 2$ with weaker computational power. $\mathbf{F_{at}}$ is defined by restricting instantiation to atomic variables only. It turns out that the type system is still sufficiently powerful to possess embeddings of full intuitionistic propositional calculus
3,
4, and since the calculus has fewer connectives and strong normalizability is simple to prove
3, this result allows us to circumvent many of the extra computational complexities present when dealing with the proof theory of IPC. It is natural to inquire whether type inhabitation, i.e. provability in the corresponding fragment of second-order intuitionistic propositional logic, is decidable or not and in general to see whether the negative results involving the undecidability of type inhabitation, typability and type-checking for $\mathbf{F}$ still hold in this fragment. A further theme would be to study the result of adding type constructors, recursors or even dependent types to $\mathbf{F_{at}}$. In this paper, we show that type inhabitation for $\mathbf{F_{at}}$ is undecidable by codifying within it an undecidable fragment of first-order intuitionistic predicate calculus, adapting and modifying the technique of Urzyczyn’s
1,
7 purely syntactic proof of the undecidability of type inhabitation for $\mathbf{F}$.
The theory of classical realizability is a framework for the Curry-Howard
correspondence which enables to associate a program with each proof in
Zermelo-Fraenkel set theory. But, almost all the ...applications of mathematics in
physics, probability, statistics, etc. use Analysis i.e. the axiom of dependent
choice (DC) or even the (full) axiom of choice (AC). It is therefore important
to find explicit programs for these axioms. Various solutions have been found
for DC, for instance the lambda-term called "bar recursion" or the instruction
"quote" of LISP. We present here the first program for AC.
We present natural deduction systems and associated modal lambda calculi for the necessity fragments of the normal modal logics K, T, K4, GL and S4. These systems are in the dual-context style: they ...feature two distinct zones of assumptions, one of which can be thought as modal, and the other as intuitionistic. We show that these calculi have their roots in in sequent calculi. We then investigate their metatheory, equip them with a confluent and strongly normalizing notion of reduction, and show that they coincide with the usual Hilbert systems up to provability. Finally, we investigate a categorical semantics which interprets the modality as a product-preserving functor.
The modal logic S4 can be used via a Curry–Howard style correspondence to obtain a λ-calculus. Modal (boxed) types are intuitively interpreted as ‘closed syntax of the calculus’. This λ-calculus is ...called modal type theory—this is the basic case of a more general contextual modal type theory, or CMTT.
CMTT has never been given a denotational semantics in which modal types are given denotation as closed syntax. We show how this can indeed be done, with a twist. We also use the denotation to prove some properties of the system.
PDF
