Related papers: Circular Proofs as Session-Typed Processes: A Loca…
We present a proof system for a multimodal logic, based on our previous work on a multimodal Martin-Loef type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e. a small 2-category.…
In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard…
This paper elaborates on a new approach of the question of the proof-theoretic study of concurrent interaction called "proofs as schedules". Observing that proof theory is well suited to the description of confluent systems while…
We introduce an infinitary first order linear logic with least and greatest fixed points. To ensure cut elimination, we impose a validity condition on infinite derivations. Our calculus is designed to reason about rich signatures of…
Game semantics extends the Curry-Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this…
Linear logic (LL) has inspired the design of many computational systems, offering reasoning techniques built on top of its meta-theory. Since its inception, several connections between concurrent systems and LL have emerged from different…
The lambda-PRK-calculus is a typed lambda-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend lambda-PRK to…
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…
Functional languages with strong static type systems have beneficial properties to help ensure program correctness and reliability. Surprisingly, their practical significance in applications is low relative to other languages lacking in…
We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic proofs and, by the Curry-Howard correspondence, into the domain of typed functional…
Taha and Nielsen have developed a multi-stage calculus {\lambda}{\alpha} with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated,…
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…
We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative extension of binary session types, which structure the type…
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.…
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,…
The Curry-Howard Correspondence has a long history, and still is a topic of active research. Though there are extensive investigations into the subject, there doesn't seem to be a definitive formulation of this result in the level of…
We propose a logic of interactive proofs as a framework for an intuitionistic foundation for interactive computation, which we construct via an interactive analog of the Goedel-McKinsey-Tarski-Artemov definition of Intuitionistic Logic as…
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the…
Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cyclic proofs with traditional finite proofs: we extend abstract…
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…