arXiv subjects

Eike Ritter

Publications and source records attributed to Eike Ritter.

5 recordsLinked to original sources

arXiv2026

Continuations and Completeness in Proof-theoretic Semantics

This is a short paper about the relationship between logic and computation. More specifically, it is about a relationship between the completeness proof for intuitionistic propositional logic within the form of proof-theoretic semantics that is known as base-extension semantics and a fundamental idea from the theory of computation called continuation-passing semantics. The latter is explained herein both in terms of reduction in natural deduction and the lambda calculus and in terms of proof-search. The relationship between completeness and continuations is explored through an analysis of Sandqvist's proof of the completeness theorem as seen from the mathematical perspective of Kripke's and Heyting's semantics. Our analysis can be seen to reveal how syntactic representations of continuations embody intensional semantical intuitions about the relationship between their meaning and use. These intuitions are made precise using the tools of proof-theoretic semantics.

math.LO↗

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↗

arXiv2024

Categorical Proof-Theoretic Semantics

In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic (IPL) raises some technical and conceptual issues. We relate Sandqvist's (complete) base-extension semantics of intuitionistic propositional logic to categorical proof theory in presheaves, reconstructing categorically the soundness and completeness arguments, thereby demonstrating the naturality of Sandqvist's constructions. This naturality includes Sandqvist's treatment of disjunction that is based on its second-order or elimination-rule presentation. These constructions embody not just validity, but certain forms of objects of justifications. This analysis is taken a step further by showing that from the perspective of validity, Sandqvist's semantics can also be viewed as the natural disjunction in a category of sheaves.

math.LO↗

arXiv2014

Verification of agent knowledge in dynamic access control policies

We develop a modeling technique based on interpreted systems in order to verify temporal-epistemic properties over access control policies. This approach enables us to detect information flow vulnerabilities in dynamic policies by verifying the knowledge of the agents gained by both reading and reasoning about system information. To overcome the practical limitations of state explosion in model-checking temporal-epistemic properties, we introduce a novel abstraction and refinement technique for temporal-epistemic safety properties in ACTLK (ACTL with knowledge modality K) and a class of interesting properties that does fall in this category.

cs.LO↗

arXiv2011

Formal Analysis of UMTS Privacy

The ubiquitous presence of mobile communication devices and the continuous development of mo- bile data applications, which results in high level of mobile devices' activity and exchanged data, often transparent to the user, makes privacy preservation an important feature of mobile telephony systems. We present a formal analysis of the UMTS Authentication and Key Agreement protocol, using the applied pi-calculus and the ProVerif tool. We formally verify the model with respect to privacy properties. We show a linkability attack which makes it possible, for individuals with low-cost equipment, to trace UMTS subscribers. The attack exploits information leaked by poorly designed error messages.

cs.CR↗