Searcharxiv⌕ Search

arXiv subjects

Carsten Schürmann

Publications and source records attributed to Carsten Schürmann.

8 recordsLinked to original sources
arXiv2024

Skolemisation for Intuitionistic Linear Logic

Focusing is a known technique for reducing the number of proofs while preserving derivability. Skolemisation is another technique designed to improve proof search, which reduces the number of back-tracking steps by representing dependencies on the term level and instantiate witness terms during unification at the axioms or fail with an occurs-check otherwise. Skolemisation for classical logic is well understood, but a practical skolemisation procedure for focused intuitionistic linear logic has been elusive so far. In this paper we present a focused variant of first-order intuitionistic linear logic together with a sound and complete skolemisation procedure.

cs.LO↗
arXiv2023

A Logical Interpretation of Asynchronous Multiparty Compatibility

Session types are types for specifying the protocols that communicating processes must follow in a concurrent system. When composing two or more well-typed processes, a session typing system must check whether such processes are multiparty compatible, a property that guarantees that all sent messages are eventually received and no deadlock ever occurs. Previous work has shown that duality and the more general notion of coherence are sufficient syntactic conditions for guaranteeing the multiparty compatibility property. In this paper, following a propositions-as-types fashion which relates session types to linear logic, we generalise coherence to forwarders. Forwarders are processes that act as middleware by forwarding messages according to a given protocol. Our main result shows that forwarders not only generalise coherence, but fully capture all well-typed multiparty compatible processes.

cs.LO↗
arXiv2021

Forwarders as Process Compatibility, Logically

Session types define protocols that processes must follow when communicating. The special case of binary session types, i.e. type annotations of protocols between two parties, is known to be in a propositions-as-types correspondence with linear logic. In previous work, we have shown that the generalization to multiparty session types can be expressed either by coherence proofs or by arbiters, processes that act as middleware by forwarding messages according to the given protocol. In this paper, following the propositions-as-types fashion, we generalize arbiters to a logic, which we call forwarder logic, a fragment of classical linear logic still satisfying cut-elimination. Our main result is summarized as follows: forwarders generalize coherence and give an elegant proof-theoretic characterization of multiparty compatibility, a property of concurrent systems guaranteeing that all sent messages are eventually received and no deadlock ever occurs.

cs.PL↗
arXiv2021

Voter Perceptions of Trust in Risk-Limiting Audits

Risk-limiting audits (RLAs) are expected to strengthen the public confidence in the correctness of an election outcome. We hypothesize that this is not always the case, in part because for large margins between the winner and the runner-up, the number of ballots to be drawn can be so small that voters lose confidence. We conduct a user study with 105 participants resident in the US. Our findings confirm the hypothesis, showing that our study participants felt less confident when they were told the number of ballots audited for RLAs. We elaborate on our findings and propose recommendations for future use of RLAs.

cs.CY↗
arXiv2021

Synchronous Forwarders

Session types are types for specifying protocols that processes must follow when communicating with each other. Session types are in a propositions-as-types correspondence with linear logic. Previous work has shown that a multiparty session type, a generalisation of session types to protocols of two or more parties, can be modelled as a proof of coherence, a generalisation of linear logic duality. And, protocols expressed as coherence can be simulated by arbiters, processes that act as a middleware by forwarding messages according to the given protocol. In this paper, we generalise the concept of arbiter to that of synchronous forwarder, that is a processes that implements the behaviour of an arbiter in several different ways. In a propositions-as-types fashion, synchronous forwarders form a logic equipped with cut elimination which is a special restriction of classical linear logic. Our main result shows that synchronous forwarders are a characterisation of coherence, i.e., coherence proofs can be transformed into synchronous forwarders and, viceversa, every synchronous forwarder corresponds to a coherence proofs.

cs.PL↗
arXiv2015

Proceedings First International Workshop on Focusing

This volume constitutes the proceedings of WoF'15, the First International Workshop on Focusing, held on November 23rd, 2015 in Suva, Fiji. The workshop was a half-day satellite event of LPAR-20, the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning. The program committee selected four papers for presentation at WoF'15, and inclusion in this volume. In addition, the program included an invited talk by Elaine Pimentel. Focusing is a proof search strategy that alternates two phases: an inversion phase where invertible sequent rules are applied exhaustively and a chaining phase where it selects a formula and decomposes it maximally using non-invertible rules. Focusing is one of the most exciting recent developments in computational logic: it is complete for many logics of interest and provides a foundation for their use as programming languages and rewriting calculi.

cs.LO↗
arXiv2011

A Bigraph Relational Model

In this paper, we present a model based on relations for bigraphical reactive systems [Milner09]. Its defining characteristics are that validity and reaction relations are captured as traces in a multi-set rewriting system. The relational model is derived from Milner's graphical definition and directly amenable to implementation.

cs.LO↗